nyuuzyou/wikis huggingface dataset:
Compact in Subspace is Compact in Topological Space

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $K \subseteq S$ be a subset.
Let $\tau_K$ be the subspace topology on $K$.
Let $T' = \struct {K, \tau_K}$ be the topological subspace of $T$ determined by $K$.
Let $H \subseteq K$ be compact in $T'$.
Then $H$ is compact in $T$.
== Proof ==
Suppose that $H$ is compact in $T'$.
Let $\set {W_i}_{i \mathop \in J}$ be an open cover of $H$ in $T$.
Then $\ds H \subseteq \bigcup_{i \mathop \in J} W_i$.
Then: 
Since $W_i \cap K \in \tau_K$, $\set {W_i \cap K}_{i \mathop \in J}$ is an open cover of $H$ in $T'$.
Since $H$ is compact in $T'$, $\set {W_i \cap K}_{i \mathop \in J}$ has some finite subcover $\set {W_i \cap K}_{i \mathop = 1}^r$.
Therefore:
So $\set {W_i}_{i \mathop = 1}^r$ is an open cover of $H$ in $T$, which is a finite subcover.
As $\set {W_i}_{i \mathop \in J}$ is arbitrary:
Any open cover of $H$ has a finite subcover in $T$.
So $H$ is compact in $T$.
Category:Compact Spaces
Category:Topological Subspaces
Compactness Properties Preserved under Continuous Mapping/Mistake

== Source Work ==
:
:Part $\text I$: Basic Definitions
::Section $3$. Compactness
:::Invariance Properties
== Mistake ==
:To be precise, the properties of compactness, $\sigma$-compactness, countable compactness, sequential compactness, Lindelöf, and separability are preserved under continuous maps ... [Weak] local compactness, and first and second countability are preserved under open continuous maps, but not just under continuous maps ...
These statements are inaccurate.
In order for a mapping to preserve these properties, it also needs to be surjective.
As an illustrative example, consider the inclusion mapping from $\closedint 0 1$ (which is compact), to $\R$ (which is not).
== Also see ==
* Compactness Properties Preserved under Continuous Surjection
* Weak Local Compactness is Preserved under Open Continuous Surjection
* Local Compactness is Preserved under Open Continuous Surjection
* Countability Axioms Preserved under Open Continuous Surjection
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Invariance Properties
Category:Mistakes/Counterexamples in Topology
Compactness Properties Preserved under Continuous Surjection

== Theorem ==
Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a continuous surjection.
If $T_A$ has one of the following properties, then $T_B$ has the same property:
:Compact Space
:$\sigma$-Compact Space
:Countable Compact Space
:Sequential Compact Space
:Lindelöf Space
== Proof ==
=== Proof for Compactness ===
=== Proof for $\sigma$-Compactness ===
=== Proof for Countable Compactness ===
=== Proof for Sequential Compactness ===
=== Proof for Lindelöf Property ===
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Invariance Properties
Category:Compact Spaces
Category:Continuous Mappings
Category:Surjections
Compactness Properties Preserved under Projection Mapping

== Theorem ==
Let $I$ be an indexing set with countable cardinality.
Let $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be a family of topological spaces indexed by $I$.
Let $\ds \struct {S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$.
Let $\pr_\alpha: \struct {S, \tau} \to \struct {S_\alpha, \tau_\alpha}$ be the projection on the $\alpha$ coordinate.
Then $\pr_\alpha$ preserves the following compactness properties.
That is, if $\struct {S, \tau}$ has one of the following properties, then each of $\struct {S_\alpha, \tau_\alpha}$ has the same property:
:Compact Space
:$\sigma$-Compact Space
:Countably Compact Space
:Sequentially Compact Space
:Lindelöf Space
:Locally Compact Space
:Weakly Locally Compact Space
:Paracompact Space
== Proof ==
First note that Projection from Product Topology is Continuous.
Also note that Projection is Surjection.
It follows from Compactness Properties Preserved under Continuous Surjection that:
:Compact Space
:$\sigma$-Compact Space
:Countably Compact Space
:Sequentially Compact Space
:Lindelöf Space
are all preserved under projections.
Next note that Projection from Product Topology is Open.
It follows from Local Compactness is Preserved under Open Continuous Surjection that local compactness is preserved under projections.
It follows from Weak Local Compactness is Preserved under Open Continuous Surjection that weak local compactness is preserved under projections.
The final result is that Paracompactness is Preserved under Projections.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Invariance Properties
Category:Compact Spaces
Category:Continuous Mappings
Category:Projections
Compactness Properties in Hausdorff Spaces

== Theorem ==
Let $P_1$ and $P_2$ be compactness properties and let:
:$P_1 \implies P_2$
mean:
:If a $T_2$ (Hausdorff) space $T$ satsifies property $P_1$, then $T$ also satisfies property $P_2$.
Then the following sequence of implications holds:
Fully $T_4$ 		$\iff$ 		Paracompact 	
 		 		$\Big\Downarrow$ 	
Weakly $\sigma$-Locally Compact 		$\implies$		$T_4$ 	
$\Big\Downarrow$ 		 		$\Big\Downarrow$ 	
Weakly Locally Compact 		$\implies$		$T_{3 \frac 1 2}$	
 		 		$\Big\Downarrow$ 	
First-Countable and Countably Compact		$\implies$		$T_3$ 	
== Proof ==
From $T_2$ Space is $T_1$ Space and $T_1$ Space is $T_0$ Space, we note that in a $T_2$ (Hausdorff) space:
:A fully $T_4$ space is a fully normal space
:A $T_4$ space is a normal space
:A $T_{3 \frac 1 2}$ space is a Tychonoff space
:A $T_3$ space is a regular space
all by definition.
From Hausdorff Space is Fully $T_4$ iff Paracompact we have that:
:Fully $T_4$ $\iff$ Paracompact.
From that same result and Fully $T_4$ Space is $T_4$ Space:
:Paracompact $\implies$ $T_4$
From Normal Space is Tychonoff Space it follows that:
:$T_4$ $\implies$ $T_{3 \frac 1 2}$
From First-Countable Space is Sequentially Compact iff Countably Compact and Sequentially Compact Hausdorff Space is Regular it follows that:
:First-Countable and Countably Compact $\implies$ $T_3$
The further justifications are listed as follows:
:$\sigma$-Locally Compact Hausdorff Space is $T_4$
:Weakly $\sigma$-Locally Compact implies Weakly Locally Compact by definition.
:$T_{3 \frac 1 2}$ Space is $T_3$ Space
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Compactness Properties and the $T_i$ Axioms
Category:Hausdorff Spaces
Category:Compact Spaces
Compactness Properties in T3 Spaces

== Theorem ==
Let $P_1$ and $P_2$ be compactness properties and let:
:$P_1 \implies P_2$
mean:
:If a $T_3$ space $T$ satsifies property $P_1$, then $T$ also satisfies property $P_2$.
Then the following sequence of implications holds:
Second-Countable		$\implies$		Lindelöf 	
$\Big\Downarrow$		 		$\Big\Downarrow$ 	
$\Downarrow$ 		 		Fully $T_4$ $\iff$ Paracompact	
$\Big\Downarrow$		 		$\Big\Downarrow$ 	
$T_5$ 		$\implies$		$T_4$ 	
== Proof ==
The justifications are listed as follows:
:Second-Countable $T_3$ Space is $T_5$
:Second-Countable Space is Lindelöf
:Lindelöf $T_3$ Space is Paracompact
:$T_3$ Space is Fully $T_4$ iff Paracompact
:Fully $T_4$ Space is $T_4$ Space
:$T_5$ Space is $T_4$ Space
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Compactness Properties and the $T_i$ Axioms
Category:T3 Spaces
Category:Compact Spaces
Compactness Theorem

== Theorem ==
Let $\LL$ be the language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then $T$ is satisfiable $T$ is finitely satisfiable.
== Proof ==
By definition, $T$ is finitely satisfiable means that every finite subset of $T$ is satisfiable.
Because the direction:
:$T$ satisfiable implies $T$ finitely satisfiable
is trivial, the proofs below all justify the converse:
:$T$ finitely satisfiable implies $T$ satisfiable.
== Proof using Consistency Principle ==
== Proof using Ultraproducts ==
== Proof using Gödel's Completeness Theorem ==
== Proof using Henkin Construction ==
== Also see ==
* Overflow Theorem
* The Class of Finite Models is not $\Delta$-Elementary
* Existence of Non-Standard Models of Arithmetic
== Sources ==
* : $\text {II}.7$ First-Order Logic Semantics: Theorem $\text {II}.7.15$
Category:Compactness Theorem
Category:Model Theory for Predicate Logic
Category:Mathematical Logic
Category:Named Theorems
Compactness Theorem/Proof using Consistency Principle

== Theorem ==
== Proof ==
By definition, $T$ is finitely satisfiable means that every finite subset of $T$ is satisfiable.
Because the direction:
:$T$ satisfiable implies $T$ finitely satisfiable
is trivial, the proof below justifies the converse:
:$T$ finitely satisfiable implies $T$ satisfiable.
By Extend Theory to Satisfy Witness Property, there exist a language $\LL^*$ and a set of $\LL^*$-sentences $T^*$ satisfying:
* $T^*$ is finitely satisfiable
* If $T^*$ is satisfiable, then $T$ is satisfiable
* For every $\LL^*$-WFF of $1$ free variable $\map \phi x$, there exists some constant $c_\phi$ such that:
::$T^* \models \paren {\exists x: \map \phi x} \implies \map \phi {x := c_\phi}$
Thus, it suffices to show that $T^*$ is satisfiable.
By Finitely Satisfiable Set of Sentences has Maximal Finitely Satisfiable Extension, there exists a set of $\LL^*$-sentences $T' \supseteq T^*$ such that:
:For all $\LL^*$-sentences $\phi$, either $\phi \in T'$ or $\sqbrk {\neg \phi} \in T'$
As $T^* \subseteq T'$, it follows that the third property above continues to hold for $T'$.
Thus, by the lemma to Extend Theory to Satisfy Witness Property:
:$T'$ satisfies the witness property
Additionally, any $\mathrm{PL}$-structure that models $T'$ will also model $T^*$.
But, by Maximal Finitely Satisfiable Theory with Witness Property is Satisfiable, there is such a $\mathrm{PL}$-structure.
Category:Compactness Theorem
Compactness Theorem/Proof using Gödel's Completeness Theorem

== Theorem ==
== Proof ==
By definition, $T$ is finitely satisfiable means that every finite subset of $T$ is satisfiable.
Because the direction:
:$T$ satisfiable implies $T$ finitely satisfiable
is trivial, the proof below justifies the converse:
:$T$ finitely satisfiable implies $T$ satisfiable.
This proof is by contraposition.
The idea is to exploit the finiteness of proofs and the relation between satisfiability and deducibility to show that if $T$ is not satisfiable, then it must have a finite subset which can be used to prove to a contradiction.
Suppose $T$ is not satisfiable.
Since $T$ has no models, it vacuously follows that $T \models \phi \wedge \neg \phi$ for some sentence $\phi$.
By Gödel's Completeness Theorem, this implies that $\phi \wedge \neg \phi$ is deducible from $T$.
But any deduction from $T$ involves only finitely many sentences from $T$.
This means that there is a finite subset $\Delta$ of $T$ such that $\phi \wedge \neg \phi$ is deducible from $\Delta$.
By Soundness of First-Order Logic, this means that $\Delta \models \phi \wedge \neg \phi$.
Thus $\Delta$ is not satisfiable.
By the Rule of Transposition, $\Delta$ is satisfiable implies $T$ is satisfiable.
== Sources ==
* : $\text {II}.7$ First-Order Logic Semantics: Theorem $\text {II}.7.15$
Category:Compactness Theorem
Category:Proofs by Contraposition
Compactness Theorem/Proof using Henkin Construction

== Theorem ==
== Proof ==
By definition, $T$ is finitely satisfiable means that every finite subset of $T$ is satisfiable.
Because the direction:
:$T$ satisfiable implies $T$ finitely satisfiable
is trivial, the proof below justifies the converse:
:$T$ finitely satisfiable implies $T$ satisfiable.
This proof actually demonstrates a stronger form of the Compactness Theorem by showing:
:If $T$ is finitely satisfiable and $\kappa$ is an infinite cardinal such that $\kappa > \size \LL$, then $T$ is satisfiable by a model whose cardinality is at most $\kappa$.
This is stronger than the original statement, since it provides extra information about the model that is claimed to exist.
The proof is said to use a Henkin Construction because it involves the construction of a model all of whose elements are interpretations of the constant symbols of some language.
Such a model was used in 's proof of the Completeness Theorem.
This special feature of the constructed model is what allows us to control its cardinality.
First, by Extend Theory to Satisfy Witness Property, we can extend $\LL$ and $T$ to find a language $\LL^*$ of cardinality at most $\kappa$ and an $\LL^*$-theory $T^*$ such that all finitely satisfiable $\LL^*$-theories containing $T^*$ have the witness property.
Then, since finitely satisfiable theories have maximal finitely satisfiable extensions, we can find a finitely satisfiable $\LL^*$-theory $T'$ containing $T^*$ such that $T'$ contains either $\phi$ or $\neg\phi$ for each $\LL^*$-sentence $\phi$.
Note that $T'$ has the witness property since it contains $T^*$.
Finally, by Maximal Finitely Satisfiable Theory with Witness Property is Satisfiable, $T'$ has a model.
Moreover, since $\LL^*$ has cardinality at most $\kappa$ and hence has at most $\kappa$-many constant symbols, this theorem ensures that the model of $T'$ can be taken to have cardinality at most $\kappa$.
== Sources ==
* : $\text {II}.7$ First-Order Logic Semantics: Theorem $\text {II}.7.15$
Category:Compactness Theorem
Compactness Theorem/Proof using Ultraproducts

== Theorem ==
== Proof ==
By definition, $T$ is finitely satisfiable means that every finite subset of $T$ is satisfiable.
Because the direction:
:$T$ satisfiable implies $T$ finitely satisfiable
is trivial, the proof below justifies the converse:
:$T$ finitely satisfiable implies $T$ satisfiable.
The idea is to construct an ultraproduct using a purposefully selected ultrafilter and collection of models so that each sentence in $T$ will be realized as a result of Łoś's Theorem.
Let $\Sigma$ be the set of all finite subsets of $T$.
For every $\Sigma_0 \in \Sigma$, define:
:$F_{\Sigma_0} = \set {\Delta \in \Sigma: \Sigma_0 \subseteq \Delta}$
That is, $F_{\Sigma_0}$ is the collection of all finite subsets of $T$ including $\Sigma_0$.
Clearly $F_{\Sigma_0}$ is a subset of $\Sigma$.
Now define:
:$F = \set {F_{\Sigma_0}: \Sigma_0 \in \Sigma}$
a subset of $\powerset \Sigma$.
We claim this has the finite intersection property.
Take any finite collection $\ds \set {F_{\Sigma_k} }_{k = 1, 2, \dots, n}$ of elements on $F$, and observe that the set $\ds S = \bigcup_{k \mathop = 1}^n \Sigma_k$ is a finite subset of $T$.
That is, $S \in \Sigma$.
$S \in F_{\Sigma_k}$ for each $k$ by construction, and hence is in their intersection.
In fact, their intersection is $F_S$.
So the intersection of any finite collection of elements of $F$ is nonempty as claimed.
Since $F$, which is a set of subsets of $\Sigma$, has the finite intersection property, there is an ultrafilter $U$ on $\Sigma$ including it (by the corollary to the Ultrafilter Lemma). 
If $\Sigma_0 \in \Sigma$, then by assumption it has a model $\AA_{\Sigma_0}$.
Define:
:$\ds \AA = \paren {\prod_{\Sigma_k \mathop \in \Sigma} \AA_{\Sigma_k} } / U$
We verify $\AA \models T$.
Take any $\phi \in T$.
Observe that $F_{\set \phi} \in U$ by definition of $U$.
Furthermore, if we define $\Phi = \set {\Sigma_0 \in \Sigma: \AA_{\Sigma_0} \models \phi}$, we have $F_{\set \phi} \subseteq \Phi$.
Hence, since $U$ is a filter and $F_{\set \phi} \in U$, $\Phi \in U$.
Then Łoś's Theorem implies that $\AA \models \phi$.
== Sources ==
* : $\text {II}.7$ First-Order Logic Semantics: Theorem $\text {II}.7.15$
Category:Compactness Theorem
Compactness Theorem for Boolean Interpretations

== Theorem ==
Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Suppose $\mathbf H$ is finitely satisfiable for boolean interpretations.
That is, suppose that every finite subset $\mathbf H' \subseteq \mathbf H$ is satisfiable for boolean interpretations.
Then $\mathbf H$ has a model.
== Proof 1 ==
== Proof 2 ==
== Also known as ==
This result is also known as the Compactness Theorem of Propositional Logic, but as there are multiple semantics for propositional logic, this name is too general to be used on .
== Sources ==
* : $\mathrm{II}.7$ First-Order Logic Semantics: Exercise $\mathrm{II.7.18}$
Category:Compactness Theorem for Boolean Interpretations
Category:Propositional Tableaux
Category:Named Theorems
Compactness Theorem for Boolean Interpretations/Proof 1

== Theorem ==
== Proof ==
Suppose $\mathbf H$ does not have a model.
By the Main Lemma of Propositional Tableaux, $\mathbf H$ has a tableau confutation $T$.
By Tableau Confutation contains Finite Tableau Confutation, $T$ may be assumed to be finite.
Hence the set $\mathbf H'$ of all WFFs in $\mathbf H$ used somewhere in $T$ is finite.
Now, let $T'$ be the labeled tree which is the same as $T$ but with root $\mathbf H'$ instead of $\mathbf H$.
Then $T'$ is a tableau confutation of $\mathbf H'$.
By the Tableau Confutation implies Unsatisfiable, $\mathbf H'$ has no models.
But this contradicts the assumption that all finite subsets of $\mathbf H$ have models.
Hence the result.
== Sources ==
* : $\S 1.11$: Compactness: Theorem $1.11.5$
Category:Compactness Theorem for Boolean Interpretations
Compactness Theorem for Boolean Interpretations/Proof 2

== Theorem ==
== Proof ==
If $\mathbf H$ is finite, the result is trivial.
So let $\mathbf H = \set {\mathbf A_n: n \in \N}$ be an enumeration of $\mathbf H$.
Define $\mathbf H_m = \set {\mathbf A_n: n \le m}$.
Let $T_1$ be the propositional tableau consisting of only a root node with hypothesis set $\mathbf H_1$.
For each $m \in \N$, construct $T_{m + 1}$ from $T_m$ by applying the Tableau Extension Lemma to $\mathbf H_{m + 1}$.
This provides us with a sequence $\sequence {T_m}_{m \mathop \in \N}$ of finished propositional tableaus.
The $T_m$ form an exhausting sequence of sets for the infinite propositional tableau $\ds T = \bigcup_{m \mathop = 1}^\infty T_m$.
If $T$ has a finished branch $\Gamma$, then by Finished Branch Lemma: Corollary:
:$\Phi \sqbrk \Gamma$ is satisfiable
and hence $\mathbf H$ is satisfiable (since $\mathbf H \subseteq \Phi \sqbrk \Gamma$).
Suppose $T$ has no finite finished branches.
Let $T'$ be the subtree of $T$ given by:
:$t \in T'$ $t$ is on a finished branch $\Gamma_m$ of every $T_m$ such that $t \in T_m$
Suppose the root node $r_T$ of $T$ were not in $T'$.
Then for some $T_m$, $r_T$ would not be on a finished branch of $T_m$.
But since $T_m$ is finished, every branch of $T_m$ is finished or contradictory.
Hence every branch of $T_m$ is contradictory.
But then $T_m$ is a tableau confutation of $\mathbf H_m$.
By Tableau Confutation implies Unsatisfiable, this contradicts the assumption that $\mathbf H_m$ is satisfiable.
Therefore, $r_T$ is in $T'$.
Suppose $T'$ were finite.
Let $t$ be a leaf of $T'$, which exists by Finite Tree has Leaf Nodes.
Suppose $t$ were a leaf of $T$.
Then $\Gamma_t$, the branch of $T$ identified by Leaf of Rooted Tree is on One Branch, is finished.
For, as any $T_m$ is a subtree of $T$, $\Gamma_t$ is the only branch of $T_m$ such that $t \in \Gamma_t$.
The conclusion follows from the definition of $T'$.
But then $\Gamma_t$ would be a finite finished branch of $T$, a contradiction.
Therefore, $T'$ cannot be finite.
Hence, $T'$ is a finitely branching tree.
By König's Tree Lemma, $T'$ has an infinite branch $\Gamma$.
By definition of $T'$, the branch $\Gamma_m := \Gamma \cap T_m$ of $T_m$ is finished for each $m \in \N$.
If $\Gamma$ were contradictory, then $\mathbf A \in \Gamma$ and $\neg\mathbf A \in \Gamma$ for some WFF $\mathbf A$.
But then $\mathbf A, \neg \mathbf A \in \Gamma_m$ for some $m \in \N$, contradicting that $\Gamma_m$ is finished.
Also, if $\mathbf A$ occurs on $\Gamma$, then it occurs on some $\Gamma_m$.
Since $\Gamma_m$ is finished, it follows that $\mathbf A$ is used on $\Gamma_m$, and hence on $\Gamma$.
In conclusion, $\Gamma$ is finished.
As established above, it follows that $\mathbf H$ is satisfiable for boolean interpretations.
Category:Compactness Theorem for Boolean Interpretations
Compactness and Sequential Compactness are Equivalent in Metric Spaces

== Theorem ==
Let $\struct {X, d}$ be a metric space. 
Then $\struct {X, d}$ is compact it is sequentially compact.
== Proof ==
=== Necessary Condition ===
This is precisely Compact Subspace of Metric Space is Sequentially Compact in Itself.
=== Sufficient Condition ===
This is precisely Sequentially Compact Metric Space is Compact.
Category:Sequentially Compact Spaces
Category:Compact Spaces
Compactness is Preserved under Continuous Surjection

== Theorem ==
Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a continuous surjection.
If $T_A$ is compact, then $T_B$ is also compact.
== Proof ==
Let $T_A$ be compact.
Take an open cover $\UU$ of $T_B$.
From Preimage of Cover is Cover, $\set {\phi^{-1} \sqbrk U: U \in \UU}$ is a cover of $S_A$.
But $\phi$ is continuous, and for all $U \in \UU$, $U$ is open in $T_B$.
It follows that $\forall U \in \UU: \phi^{-1} \sqbrk U$ is open in $T_A$.
So $\set {\phi^{-1} \sqbrk U:\ U \in \UU}$ is an open cover of $T_A$.
$T_A$ is compact, so we take a finite subcover:
:$\set {\phi^{-1} \sqbrk {U_1}, \ldots, \phi^{-1} \sqbrk {U_n} }$
We have that $\phi$ is surjective.
So from Surjection iff Right Inverse, $\phi \sqbrk {\phi^{-1} \sqbrk A} = A$
So:
:$\set {\phi \sqbrk {\phi^{-1} \sqbrk {U_1} }, \ldots, \phi \sqbrk {\phi^{-1} \sqbrk {U_n} } } = \set {U_1, \ldots, U_n} \subseteq \UU$
is a finite subcover of $\UU$ on $T_B$.
== Also see ==
* Compactness Properties Preserved under Continuous Surjection
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Invariance Properties
Category:Compact Spaces
Category:Continuous Mappings
Category:Surjections
Compactness of First-Order Logic

#Redirect Compactness Theorem
== Theorem ==
Let $\Gamma$ be any countable set of first-order formulas, and suppose every finite subset of $\Gamma$ is satisfiable.
Then $\Gamma$ is satisfiable.
== Proof ==
Suppose $\Gamma$ is unsatisfiable.
Since consistency implies satisfiability, $\Gamma$ is inconsistent, i.e., it proves a contradiction.
But first-order proofs are by definition finite, so there is some subset $\Gamma_0$ of $\Gamma$ such that $\Gamma_0$ is inconsistent.
Now since satisfiability implies consistency, $\Gamma_0$ is unsatisfiable.
Hence if all finite subsets of $\Gamma$ are satisfiable, so is $\Gamma$.
== Consequences ==
* Overflow Theorem
* The Class of Finite Models is not $\Delta$-Elementary
* Existence of Non-Standard Models of Arithmetic
Category:Mathematical Logic
Comparison Principle for Extremal Length

== Theorem ==
Let $X$ be a Riemann surface.
Let $\Gamma_1$ and $\Gamma_2$ be families of rectifiable curves (or, more generally, families of unions of rectifiable curves) on $X$.
Let every element of $\Gamma_1$ contain some element of $\Gamma_2$.
Then the extremal lengths of $\Gamma_1$ and $\Gamma_2$ are related by:
:$\lambda \left({\Gamma_1}\right) \ge \lambda \left({\Gamma_2}\right)$
More precisely, for every conformal metric $\rho$ as in the definition of extremal length, we have:
:$L \left({\Gamma_1, \rho}\right) \ge L \left({\Gamma_2, \rho}\right)$
== Proof ==
We have:
This proves the second claim.
The second claim implies the first by definition.
== Sources ==
* 
Category:Geometric Function Theory