nyuuzyou/wikis huggingface dataset:
Filter is Prime iff For Every Element Element either Negation Belongs to Filter in Boolean Lattice

== Theorem ==
Let $B = \struct {S, \vee, \wedge, \neg, \preceq}$ be a Boolean lattice.
Let $F$ be a filter in $B$.
Then
:$F$ is prime
:$\forall x \in S: x \in F \lor \paren {\neg x} \in F$
== Proof ==
=== Sufficient Condition ===
Let $F$ be prime.
Let $x \in S$.
By definition of Boolean lattice:
:$x \vee \neg x = \top$
where $\top$ denotes the top of $B$.
By definition of non-empty set:
:$\exists y: y \in F$
By definition of greatest element:
:$y \preceq \top$
By definition of upper section:
:$\top \in F$
Thus by definition of prime filter:
:$x \in F$ or $\neg x \in F$
=== Necessary Condition ===
Assume that
:$\forall x \in S: x \in F \lor \paren {\neg x} \in F$
Let $a, b \in S$ such that
:$a \vee b \in F$
:$a \notin F$ and $b \notin F$
By assumption:
:$\neg a \in F$ and $\neg b \in F$
By Filtered in Meet Semilattice:
:$\paren {\neg a} \wedge \paren {\neg b} \in F$
By De Morgan's Laws (Boolean Algebras):
:$\map \neg {a \vee b} \in F$
By Filtered in Meet Semilattice:
:$\paren {a \vee b} \wedge \map \neg {a \vee b} \in F$
By definition of Boolean lattice:
:$\bot \in F$
where $\bot$ denotes the bottom of $B$.
By definition of smallest element:
:$\bot \preceq a$
By definition of upper section:
:$a \in F$
This contradicts $a \notin F$
Thus by Proof by Contradiction
:the result holds.
== Sources ==
* 
* 
Category:Prime Ideals (Order Theory)
Category:Boolean Algebras
Filter on Product Space Converges iff Projections Converge

== Theorem ==
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of non-empty topological spaces where $I$ is an arbitrary index set.
Let $\ds X := \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Let $\pr_i: X \to X_i$ denote the projection from $X$ onto $X_i$.
Let $\FF \subset \powerset X$ be a filter on $X$.
Then $\FF$ converges for all $i \in I$ the image filter $\map {\pr_i} \FF$ converges.
== Proof ==
=== Sufficient Condition ===
Let $\FF$ converge.
Then there is a point $x \in X$ such that $\FF$ converges to $x$.
By Filter on Product Space Converges to Point iff Projections Converge to Projections of Point:
:$\forall i \in I: \map {\pr_i} \FF$ converges to $x_i$
Thus
:$\forall i \in I: \map {\pr_i} \FF$ converges.
=== Necessary Condition ===
Suppose that for each $i \in I$, $\map {\pr_i} \FF$ converges.
For each $i \in I$, let $S_i$ be the set of points to which $\map {\pr_i} \FF$ converges.
By our supposition, $S_i$ is non-empty for each $i \in I$.
By the axiom of choice, there is a point $x \in X$ such that:
:$\forall i \in I: \map {\pr_i} x \in S_i$
By Filter on Product Space Converges to Point iff Projections Converge to Projections of Point, $\FF$ converges to $x$.
== Also see ==
* Filter on Product of Hausdorff Spaces Converges iff Projections Converge, a more restricted result that does not require the axiom of choice.
Category:Topology
Category:Filter Theory
Category:Projections
Filter on Product Space Converges to Point iff Projections Converge to Projections of Point

== Theorem ==
Let $\family{X_i}_{i \mathop \in I}$ be an indexed family of non-empty topological spaces where $I$ is an arbitrary index set.
Let $\ds X := \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Let $\FF$ be a filter on $X$.
Let $x \in X$.
Let $\pr_i: X \to X_i$ denote the projection from $X$ onto $X_i$.
Then $\FF$ converges to $x$ :
:for all $i \in I$ the image filter $\map {\pr_i} \FF$ converges to $x_i := \map {\pr_i} x$.
== Proof ==
=== Necessary Condition ===
Let $\FF$ converge to $x$.
Let $i \in I$.
From Projection from Product Topology is Continuous, $\pr_i : X \to X_i$ is continuous.
Thus $\map {\pr_i} \FF$ converges to $\map {\pr_i} x$ as claimed.
=== Sufficient Condition ===
For all $i \in I$, let $\map {\pr_i} \FF$ converge to $\map {\pr_i} x$.
Let $V \subseteq X$ a neighborhood of $x$.
We have to show that $V \in \FF$.
Then there is a set $U$ from the natural basis of $X$ such that $x \in U \subseteq V$.
By the definition of the natural basis, there is a finite set $J \subseteq I$ such that:
:$\ds U = \bigcap_{j \mathop \in J} \map {\pr_j^{-1}} {U_j}$
where $U_j \subseteq X_j$ is an open set for all $j \in J$.
Thus $U_j$ is an open neighborhood of $x_j$ for all $j \in J$.
Since $\map {\pr_j} \FF$ converges to $x_j$, this implies $U_j \in \map {\pr_j} \FF$ for all $j \in J$.
By the definition of $\map {\pr_j} \FF$, this implies $\map {\pr_j^{-1}} {U_j} \in \FF$ for all $j \in J$.
Since $J$ is finite, it follows that:
:$\ds U = \bigcap_{j \mathop \in J} \map {\pr_j^{-1}} {U_j} \in \FF$
Recall that $U \subseteq V$.
As $\FF$ is a filter, this implies that also $V \in \FF$.
Thus $\FF$ converges to $x$ as claimed.
== Also see ==
* Filter on Product Space Converges iff Projections Converge
Category:Product Topology
Category:Filter Theory
Category:Projections
Filter on Product of Hausdorff Spaces Converges iff Projections Converge

== Theorem ==
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of non-empty Hausdorff spaces where $I$ is an arbitrary index set.
Let $\ds X := \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Let $\pr_i: X \to X_i$ denote the projection from $X$ onto $X_i$.
Let $\FF \subset \powerset X$ be a filter on $X$.
Then $\FF$ converges for each $i \in I$ the image filter $\map {\pr_i} \FF$ converges.
== Proof ==
=== Sufficient Condition ===
Let $\FF$ converge.
Then there is a point $x \in X$ such that $\FF$ converges to $x$.
By Filter on Product Space Converges to Point iff Projections Converge to Projections of Point:
:$\forall i \in I: \map {\pr_i} \FF$ converges to $x_i$.
Thus, for each $i \in I$, $\map {\pr_i} \FF$ converges.
=== Necessary Condition ===
For each $i \in I$, let $\map {\pr_i} \FF$ converge.
Since $X_i$ is a Hausdorff space for each $i \in I$, this implies that $\map {\pr_i} \FF$ converges to exactly one point for each $i \in I$.
For each $i$, let $x_i$ be the point in $X_i$ to which $\map {\pr_i} \FF$ converges.
Then by the definition of the product space, $x$ is an element of $X$.
By Filter on Product Space Converges to Point iff Projections Converge to Projections of Point, $\FF$ converges to $x$.
== Also see ==
* Filter on Product Space Converges iff Projections Converge, a more general result requiring the axiom of choice.
Category:Topology
Category:Filter Theory
Category:Projections
Filter on Set/Examples/Closed Real Intervals

== Examples of Filters on Sets ==
Let $\FF$ be the set of all closed real intervals $\closedint x y$ such that:
:$0 < x < \dfrac 1 2 < y < 1$
Then $\FF$ is a filter on the closed real interval $\closedint 0 1$.
== Proof ==
== Sources ==
* 
* 
Category:Examples of Filters on Sets
Filter on Set is Proper Filter

== Theorem ==
Let $S$ be a set.
Let $\powerset S$ denote the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the poset defined on $\powerset S$ by the subset relation.
Let $\FF$ be a filter on $S$.
Then $\FF$ is a proper filter on $\struct {\powerset S, \subseteq}$.
== Proof ==
From the general definition of a filter, we have:
A filter on $\struct {S, \preccurlyeq}$ is a subset $\FF \subseteq S$ which satisfies the following conditions:
:$\FF \ne \O$
:$x, y \in \FF \implies \exists z \in \FF: z \preccurlyeq x, z \preccurlyeq y$
:$\forall x \in \FF: \forall y \in S: x \preccurlyeq y \implies y \in \FF$
A filter $\FF$ is proper if it does not equal $S$ itself.
From the definition of a filter on a set, we have:
A filter on $T$ is a set $\FF \subset \powerset T$ which satisfies the following conditions:
:$T \in \FF$
:$\O \notin \FF$
:$U, V \in \FF \implies U \cap V \in \FF$
:$\forall U \in \FF: U \subseteq V \subseteq T \implies V \in \FF$
We can identify:
:$\powerset T$ with $S$
:$\subseteq$ with $\preccurlyeq$.
=== Filter Not Empty ===
We have that $T \in \FF$ and so $\FF \ne \O$.
=== Preceding Elements in Filter ===
We have that:
:$U, V \in \FF \implies U \cap V \in \FF$
From Intersection is Subset, we have that $U \cap V \subseteq U$ and $U \cap V \subseteq V$.
So identifying $U$ with $x$, $V$ with $y$ and $U \cap V$ with $z$ it is clear that:
:$x, y \in \FF \implies \exists z \in \FF: z \preccurlyeq x, z \preccurlyeq y$
=== Succeeding Elements in Filter ===
We have that:
:$\forall U \in \FF: U \subseteq V \subseteq T \implies V \in \FF$
This can be rewritten:
:$\forall U \in \FF, V \in \powerset T: U \subseteq V \implies V \in \FF$
Identifying $U$ with $x$ and $V$ with $y$, this translates as:
:$\forall x \in \FF, y \in S: x \preccurlyeq y \implies y \in \FF$
=== Proper Filter ===
For $\FF$ to be a proper filter on $\struct {\powerset T, \subseteq}$, it must not equal $\powerset T$.
This is seen to be satisfied by the axiom $\O \notin \FF$.
All axioms are fulfilled, hence the result.
== Note about Axioms ==
Category:Filter Theory
Category:Filter on Set is Proper Filter
Filter on Set is Proper Filter/Note about Axioms

== Filter on Set is Proper Filter Note about Axioms ==
It seems at first glance that the condition $T \in \FF$ is not axiomatic, as it is clear from the third property:
:$U \in \FF: U \subseteq T \subseteq T \implies T \in \FF$
However, one of the properties of a filter is that it is specifically not empty.
Specifying that $T \in \FF$ is therefore equivalent to specifying that $\FF \ne \O$.
Thus it would be possible to cite the first axiom as $\FF \ne \O$ instead, but this is rarely done.
Category:Filter on Set is Proper Filter
Filtered iff Directed in Dual Ordered Set

== Theorem ==
Let $\struct {S, \preceq_1}$ be an ordered set.
Let $\struct {S, \preceq_2}$ be a dual ordered set of $\struct {S, \preceq_1}$
Let $X \subseteq S$.
Then:
:$X$ is filtered in $\struct {S, \preceq_1}$
:
:$X$ is directed in $\struct {S, \preceq_2}$
== Proof ==
By Dual of Dual Ordering:
:$\struct {S, \preceq_1}$ is the dual of $\struct {S, \preceq_2}$.
Thus by Directed iff Filtered in Dual Ordered Set:
:$X$ is filtered in $\struct {S, \preceq_1}$
:
:$X$ is directed in $\struct {S, \preceq_2}$.
== Sources ==
* 
Category:Dual Orderings
Filtered iff Finite Subsets have Lower Bounds

== Theorem ==
Let $\struct {S, \precsim}$ be a preordered set.
Let $H$ be a non-empty subset of $S$.
Then $H$ is filtered :
:for every finite subset $A$ of $H$:
::$\exists h \in H: \forall a \in A: h \precsim a$
== Proof ==
This follows by mutatis mutandis of the proof of Directed iff Finite Subsets have Upper Bounds.
== Sources ==
* 
* 
Category:Preorder Theory
Filtered iff Upper Closure Filtered

== Theorem ==
Let $\struct {S, \precsim}$ be a preordered set.
Let $H$ be a non-empty subset of $S$.
Then $H$ is filtered 
$H^\succsim$ is filtered
where $H^\succsim$ denotes the upper closure of $H$.
== Proof ==
This follows by of the proof of Directed iff Lower Closure Directed.
== Sources ==
* 
* 
Category:Preorder Theory
Filtered in Meet Semilattice

== Theorem ==
Let $\struct {S, \preceq}$ be a meet semilattice.
Let $H$ be a non-empty upper section of $S$.
Then $H$ is filtered 
:$\forall x, y \in H: x \wedge y \in H$
== Proof ==
This follows by of the proof of Directed in Join Semilattice.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Category:Upper Sections
Filtered in Meet Semilattice with Finite Infima

== Theorem ==
Let $\struct {S, \preceq}$ be a meet semilattice.
Let $H$ be a non-empty upper section of $S$.
Then $H$ is filtered 
:for every non-empty finite subset $A$ of $H$, $\inf A \in H$
== Proof ==
This follows by of the proof of Directed in Join Semilattice with Finite Suprema.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Category:Upper Sections
Filters equal Ideals in Dual Ordered Set

== Theorem ==
Let $L_1 = \struct {S, \preceq_1}$ be an ordered set.
Let $L_2 = \struct {S, \preceq_2}$ be a dual ordered set of $L_1$.
Then $\map {\mathit {Filt} } {L_1} = \map {\mathit {Ids} } {L_2}$
where
:$\map {\mathit {Filt} } {L_1}$ denotes the set of all filters of $L_1$,
:$\map {\mathit {Ids} } {L_2}$ denotes the set of all ideals of $L_2$.
== Proof ==
Let $x$ be a set.
By definition of $\mathit {Filt}$:
:$x \in \map {\mathit {Filt} } {L_1} \iff x$ is a filter on $L_1$.
By Filter is Ideal in Dual Ordered Set:
:$x \in \map {\mathit {Filt} } {L_1} \iff x$ is an ideal in $L_2$.
By definition of $\mathit{Ids}$:
:$x \in \map {\mathit {Filt} } {L_1} \iff x \in \map {\mathit {Ids} } {L_2}$
Hence by definition of set equality:
:$\map {\mathit {Filt} } {L_1} = \map {\mathit {Ids} } {L_2}$
== Sources ==
* 
Category:Dual Orderings
Filters form Complete Lattice

== Theorem ==
Let $L = \left({S, \wedge, \preceq}\right)$ be a bounded above meet semilattice.
Let $F = \left({\mathit{Filt}\left({L}\right), \subseteq}\right)$ be an inclusion ordered set,
where $\mathit{Filt}\left({L}\right)$ denotes set of all filters on $L$.
Then $F$ is a complete lattice.
== Proof ==
Define $L^{-1} := \left({S, \succeq}\right)$ be a dual ordered set of $L$.
By Dual Pairs (Order Theory):
:$L^{-1}$ is a bounded below meet semilattice.
By Filters equal Ideals in Dual Ordered Set:
:$\mathit{Filt}\left({L}\right) = \mathit{Ids}\left({L^{-1} }\right)$
where $\mathit{Ids}\left({L^{-1} }\right)$ denotes the set of all ideals in $L^{-1}$.
Thus by Ideals form Complete Lattice:
:$F$ is a complete lattice.
== Sources ==
* 
Category:Complete Lattices
Filters of Lattice of Power Set form Bounded Above Ordered Set

== Theorem ==
Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.
Let $F = \struct {\map {\operatorname{Filt} } L, \subseteq}$ be an inclusion ordered set,
where $\map {\operatorname{Filt} } L$ denotes the set of all filters on $L$.
Then $F$ is bounded above and $\top_F = \powerset X$
where $\top_F$ denotes the greatest element of $F$.
== Proof ==
By Power Set is Filter in Lattice of Power Set:
:$\powerset X$ is a filter on $L$.
Let $A \in \map {\operatorname{Filt} } L$.
Thus by definition of filter:
:$A \subseteq \powerset X$
Thus by definitions:
:$F$ is bounded above and $\top_F = \powerset X$
== Sources ==
* 
* 
Category:Power Set
Filters of Lattice of Power Set form Bounded Below Ordered Set

== Theorem ==
Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.
Let $F = \struct {\map {\operatorname {Filt} } L, \subseteq}$ be an inclusion ordered set,
where $\map {\operatorname {Filt} } L$ denotes the set of all filters on $L$.
Then $F$ is bounded below and $\bot_F = \set X$
where $\bot_F$ denotes the smallest element of $F$.
== Proof ==
By Singleton of Set is Filter in Lattice of Power Set:
:$\set X$ is a filter on $L$.
Let $A \in \map {\operatorname {Filt} } L$.
By definition of non-empty set:
:$\exists x: x \in A$
By definition of power set:
:$x \subseteq X$
By definition of upper section:
:$X \in A$
Thus by definitions of singleton and subset:
:$\set X \subseteq A$
Thus by definitions:
:$F$ is bounded below and $\bot_F = \set X$
== Sources ==
* 
* 
Category:Power Set
Filtration's Lp Spaces are Dense in Limit Filtration's Lp Space

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\sequence {\FF_n}_{n \mathop \in \N}$ be a filtration of $\Sigma$. 
Let $\FF_\infty$ be the limit of $\sequence {\FF_n}_{n \mathop \in \N}$.
Let $p \ge 1$.
Let $\map {L^p} {\cdot}$ denote the $L^p$ spaces.
Then $\ds \bigcup_{n \mathop \ge 0} \map {L^p} {X, \FF_n, \mu}$ is a dense subset of $\map {L^p} {X, \FF_\infty, \mu}$.
== Proof ==
First, it is a subset, since
:$\forall n \ge 0 : \map {L^p} {X, \FF_n, \mu} \subseteq \map {L^p} {X, \FF_\infty, \mu}$
in view of $\FF_n \subseteq \FF_\infty$.
In the following, we show its density.
Let:
:$\ds \AA_0 := \bigcup_{n \mathop \ge 0} \FF_n$
Then $\AA_0$ is an algebra.
By Sigma-Algebra extended from Algebra by Measure:
:$\ds \BB := \bigcap_{\epsilon \mathop > 0} \bigcup_{A \mathop \in \AA_0} \set {B \in \Sigma : \map \mu {A \symdif B} \le \epsilon}$
is a $\sigma$-algebra.
In particular:
:$(1):\quad \FF_\infty = \map \sigma {\AA_0} \subseteq \BB$
Let $f \in \map {L^p} {X, \FF_\infty, \mu}$.
Let $\epsilon > 0$.
By Space of Simple P-Integrable Functions is Everywhere Dense in Lebesgue Space, there exist:
:$n \in \Z_{>0}$
:$\alpha_1, \ldots, \alpha_n \in \R_{\ne 0}$
:$B_1, \ldots, B_n \in \FF_\infty$
such that:
:$\ds (2): \quad \norm {f - \sum_{k \mathop = 1}^n \alpha_k \chi_{B_k} }_p \le \epsilon$
By $(1)$, there exist:
:$A_1, \ldots, A_n \in \AA_0$
such that:
:$\ds (3): \quad \forall k \in \set {1, \ldots, n} : \map \mu {A_k \symdif B_k} \le \paren {\frac \epsilon {\size {n \alpha _k} } }^p$
By definition of $\AA_0$, for each $k$ there exists an $n_k \ge 0$ such that:
:$A_k \in \FF_{n_k}$
Let $N := \max \set {n_1, \ldots, n_k}$.
Then:
:$A_1, \ldots, A_n \in \FF_N$
In particular:
:$\ds \sum_{k \mathop = 1}^n \alpha_k \chi_{A_k} \in \map {L^p} {X, \FF_N, \mu}$
Moreover:
Category:Filtrations of Sigma-Algebras
Category:Lp Spaces
Final Topology Contains Codomain Topology iff Mappings are Continuous

== Theorem ==
Let $\struct{Y, \tau}$ be a topological space.
Let $\family {\struct{X_i, \tau_i}}_{i \mathop \in I}$ be a family of topological spaces.
Let $\family {f_i}_{i \mathop \in I}$ be a family of mappings $f_i : X_i \to Y$.
Let $\tau'$ be the final topology on $Y$ with respect to $\family {f_i}_{i \mathop \in I}$.
Then:
:$\tau \subseteq \tau'$ $\forall i \in I : f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau}$ is continuous.
== Proof ==
=== Necessary Condition ===
Let $\tau \subseteq \tau'$.
From Equivalence of Definitions of Final Topology:
:for each $i \in I$, $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau'}$ is $\tuple{\tau_i, \tau'}$-continuous
From Continuous Mapping on Finer Domain and Coarser Codomain Topologies is Continuous:
:for each $i \in I$, $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau}$ is $\tuple{\tau_i, \tau}$-continuous
=== Sufficient Condition ===
For all $i \in I$, let $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau}$ be $\tuple{\tau, \tau_i}$-continuous.
From Equivalence of Definitions of Final Topology:
:$\tau'$ is the finest topology on $Y$ such that each $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau'}$ is $\tuple{\tau_i, \tau'}$-continuous.
Then:
:$\tau \subseteq \tau'$
Category:Final Topology
Final Topology is Topology

== Theorem ==
Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct {Y_i, \tau_i} }_{i \mathop \in I}$ be an $I$-indexed family of topological spaces.
Let $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be an $I$-indexed family of mappings.
Let $\tau$ be the final topology on $X$ with respect to $\family {f_i}_{i \mathop \in I}$.
Then $\tau$ is a topology on $X$.
== Proof ==
Define:
:$\forall i \in I: \vartheta_i = \set {U \subseteq X: \map {f_i^{-1} } U \in \tau_i} \subseteq \powerset X$
Then, by the definition of intersection:
:$\ds \tau = \bigcap_{i \mathop \in I} \vartheta_i$
From the Intersection of Topologies is Topology, it suffices to show, for all $i \in I$, that $\vartheta_i$ is a topology on $X$.
We now verify the axioms for $\vartheta_i$ to be a topology on $X$.
=== ===
Let $\AA \subseteq \vartheta_i$.
Then, by Preimage of Union under Mapping: General Result and by the definition of a topology, it follows that:
:$\ds f_i^{-1} \sqbrk {\bigcup \AA} = \bigcup_{U \mathop \in \AA} f_i^{-1} \sqbrk U \in \tau_i$
That is, $\ds \bigcup \AA \in \vartheta_i$.
=== ===
Let $U, V \in \vartheta_i$.
Then, by Preimage of Intersection under Mapping and by the definition of a topology, it follows that:
:$f_i^{-1} \sqbrk {U \cap V} = f_i^{-1} \sqbrk U \cap f_i^{-1} \sqbrk V \in \tau_i$
That is, $U \cap V \in \vartheta_i$.
=== ===
By the definition of a topology, it follows that:
:$f_i^{-1} \sqbrk X = Y_i \in \tau_i$
That is, $X \in \vartheta_i$.
All the open set axioms are fulfilled, and the result follows.
Category:Final Topology
Final Topology with respect to Mapping

== Theorem ==
Let $\struct {X, \tau_X}$ be a topological space.
Let $Y$ be a set.
Let $f: X \to Y$ be a mapping.
Let $\tau_Y$ be the final topology on $Y$ $f$.
Then:
:$\tau_Y = \set {U \subseteq Y : f^{-1} \sqbrk U \in \tau_X}$
Observe that the set on the of the equality is sometimes denoted $f\tau$.
Further, the following holds true:
# $\forall \struct {Z, \tau_Z}$ topological space $\forall g: \struct {Y, f \tau} \to \struct {Z, \tau_Z}$ mapping $g$ is continuous $\iff g \circ f$ is continuous (where $f$ is defined from $\struct {X, \tau_X}$ to $\struct {Y, f \tau}$).
# $\forall \tau_Y$ topology in $Y : \forall \struct {Z, \tau_Z}$ topological space, the following are equivalent:
##$\tau_Y = f \tau$
##$\forall g: \struct {Y, \tau_Y} \to \struct {Z, \tau_Z}: g$ is continuous $\iff g \circ f$ is continuous (where $f$ is defined from $\struct {X, \tau_X}$ to $\struct {Y, \tau_Y}$).
That is, the topology $f \tau$ is characterised by the fact that it is the only one which makes all mappings defined from it to any topological space continuous.
== Proof ==
Category:Topology
Final Value Theorem of Laplace Transform

== Theorem ==
Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of the real function $f$.
Then:
:$\ds \lim_{t \mathop \to \infty} \map f t = \lim_{s \mathop \to 0} s \, \map F s$
if those limits exist.
=== General Result ===
== Proof ==
From Laplace Transform of Derivative:
:$(1): \quad \laptrans {\map {f'} t} = s \, \map F s - \map f 0$
We have that:
Hence:
Suppose that $f$ is not continuous at $t = 0$.
From Laplace Transform of Derivative with Discontinuity at Zero:
:$\laptrans {\map {f'} t} = s \, \map F s - \map f {0^+}$
which means:
:$(3): \quad \laptrans {\map {f'} t} = s \, \map F s - \ds \lim_{u \mathop \to 0} \map f u$
We have that:
Hence:
== Examples ==
== Sources ==
* : Chapter $1$: The Laplace Transform: Some Important Properties of Laplace Transforms: $12$. Final-value theorem: Theorem $1 \text{-} 17$
* : Chapter $1$: The Laplace Transform: Solved Problems: Initial and Final Value Theorems: $26$
Category:Laplace Transforms
Final Value Theorem of Laplace Transform/Examples/Example 1

== Example of use of Initial Value Theorem of Laplace Transform ==
Consider the real function $f: \R \to \R$ defined as:
:$\map f t = 3 e^{-2 t}$
From Laplace Transform of Exponential:
:$\laptrans {\map f t} = \dfrac 3 {s + 2}$
Then by the Initial Value Theorem of Laplace Transform:
== Sources ==
* : Chapter $1$: The Laplace Transform: Solved Problems: Initial and Final Value Theorems: $27 \ \text{(b)}$
Category:Examples of Laplace Transforms
Final Value Theorem of Laplace Transform/General Result

== Theorem ==
Let $f$ and $g$ be real functions.
Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of $f$.
Let $\ds \lim_{t \mathop \to \infty} \dfrac {\map f t} {\map g t} = 1$.
Then:
:$\ds \lim_{s \mathop \to 0} \dfrac {\map F s} {\map G s} = 1$
if those limits exist.
== Proof ==
== Sources ==
* : Chapter $1$: The Laplace Transform: Some Important Properties of Laplace Transforms: $14$. Generalization of final-value theorem: Theorem $1 \text{-} 19$
Category:Laplace Transforms
Finding Center of Circle/Proof 1

== Theorem ==
== Proof ==
:
Draw any chord $AB$ on the circle in question.
Bisect $AB$ at $D$.
Construct $CE$ perpendicular to $AB$ at $D$, where $C$ and $E$ are where this perpendicular meets the circle.
Bisect $CE$ at $F$.
Then $F$ is the center of the circle.
The proof is as follows.
Suppose $F$ were not the center of the circle, but that $G$ were instead.
Join $GA, GB, GD$.
As $G$ is (as we have supposed) the center, then $GA = GB$.
Also, we have $DA = DB$ as $D$ bisects $AB$.
So from Triangle Side-Side-Side Congruence:
:$\triangle ADG = \triangle BDG$
Hence:
:$\angle ADG = \angle BDG$
But from :
:
So $\angle ADG$ is a right angle.
But $\angle ADF$ is also a right angle.
So $\angle ADG = \angle ADF$, and this can happen only if $G$ lies on $CE$.
But then as $G$ is, as we suppose, at the center of the circle, then $GC = GE$.
Thus it follows that $G$ bisects $CE$.
But then $GC = FC$, and so $G = F$.
Hence the result.
=== Porism ===
== Sources ==
* : Book $\text{III}$. Propositions
Category:Finding Center of Circle