nyuuzyou/wikis huggingface dataset:
Infima Preserving Mapping on Filters Preserves Filtered Infima

== Theorem ==
Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every filter $F$ in $\struct {S, \preceq}$, let $f$ preserve the infimum on $F$.
Then $f$ preserves filtered infima.
== Proof ==
Let $F$ be a filtered subset of $S$ such that:
:$F$ admits an infimum in $\struct {S, \preceq}$.
By Filtered iff Upper Closure Filtered:
:$F^\succeq$ is filtered
where $F^\succeq$ denotes the upper closure of $F$.
By Upper Closure is Upper Section:
:$F^\succeq$ is upper.
Because filtered is non-empty, by definition:
:$F^\succeq$ is filter in $\struct {S, \preceq}$.
By Infimum of Upper Closure of Set:
:$F^\succeq$ admits an infimum in $\struct {S, \preceq}$
and
:$\map \inf {F^\succeq} = \inf F$
By assumption and mapping preserves the infimum on subset:
:$\map {f^\to} {F^\succeq}$ admits an infimum in $\struct {T, \precsim}$
and
:$\map \inf {\map {f^\to} {F^\succeq} } = \map f {\map \inf {F^\succeq} }$
By Upper Closure is Closure Operator:
:$F \subseteq F^\succeq$
By Image of Subset under Mapping is Subset of Image:
:$\map {f^\to} F \subseteq \map {f^\to} {F^\succeq}$
By definition of infimum:
:$\map f {\inf F}$ is lower bound for $\map {f^\to} {F^\succeq}$
By Lower Bound is Lower Bound for Subset:
:$\map f {\inf F}$ is a lower bound for $\map {f^\to} F$
We will prove that:
:for every element $x$ of $T$:
::if $x$ is lower bound for $\map {f^\to} F$, then $x \precsim \map f {\inf F}$
Let $x \in T$ such that:
:$x$ is a lower bound for $\map {f^\to} \F$
We will prove as a sublemma that:
:$x$ is a lower bound for $\map {f^\to} {F^\succeq}$
Let $y \in \map {f^\to} {F^\succeq}$.
By definition of image of set under mapping:
:$\exists a \in S: a \in F^\succeq \land y = \map f a$
By definition of upper closure of set:
:$\exists b \in F: b \preceq a$
By Infima Preserving Mapping on Filters is Increasing:
:$f$ is increasing.
By definition of increasing:
:$\map f b \precsim \map f a$
By definition of image of set under mapping:
:$\map f b \in \map {f^\to} F$
By definition of lower bound of set:
:$x \precsim \map f b$
Thus by definition of transitivity:
:$x \precsim y$
Thus by definition:
:$x$ is a lower bound for $\map {f^\to} {F^\succeq}$
This ends the proof of the sublemma.
Thus by definition of infimum:
:$x \precsim \map f {\inf F}$
Thus again by definition of infimum:
:$\map {f^\to} F$ admits an infimum in $\struct {T, \precsim}$
and
:$\map \inf {\map {f^\to} F} = \map f {\inf F}$
Thus result follows by definition of mapping preserves filtered infima.
== Sources ==
* 
* 
Category:Order Theory
Infima Preserving Mapping on Filters is Increasing

== Theorem ==
Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every filter $F$ in $\struct {S, \preceq}$, let $f$ preserve the infimum on $F$.
Then $f$ is increasing.
== Proof ==
Let $x, y \in S$ such that:
:$x \preceq y$
By Infimum of Singleton:
:$\set x$ and $\set y$ admit infima in $\struct {S, \preceq}$
By Infimum of Upper Closure of Set:
:$\set x^\succeq$ and $\set y^\succeq$ admit infima in $\struct {S, \preceq}$
where $\set x^\succeq$ denotes the upper closure of $\set x$.
By Upper Closure of Singleton
:$x^\succeq$ and $y^\succeq$ admit infima in $\struct {S, \preceq}$
By Upper Closure of Element is Filter:
:$x^\succeq$ and $y^\succeq$ are filter in $\struct {S, \preceq}$
By assumption and definition of mapping preserves the infimum on subset:
:$\map {f^\to} {x^\succeq}$ and $\map {f^\to} {y^\succeq}$ admit infima in $\struct {T, \precsim}$
and
:$\inf \set {\map {f^\to} {x^\succeq} } = \map f {\inf \set {x^\succeq} }$ and $\inf \set {\map {f^\to} {y^\succeq} } = \map f {\inf \set {y^\succeq} }$
By Infimum of Upper Closure of Element:
:$\inf \set {x^\succeq} = x$ and $\inf \set {y^\succeq} = y$
By Upper Closure is Decreasing:
:$y^\succeq \subseteq x^\succeq$
By Image of Subset under Mapping is Subset of Image:
:$\map {f^\to} {y^\succeq} \subseteq \map {f^\to} {x^\succeq}$
Thus by Infimum of Subset:
:$\map f x \precsim \map f y$
Thus by definition:
:$f$ is increasing.
== Sources ==
* 
* 
Category:Order Theory
Category:Increasing Mappings
Infima in Ordered Group

== Theorem ==
Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group.
Let $x, y, z \in G$ be arbitrary.
Let any one of the sets $\set {x, y}$, $\set {x \circ z, y \circ z}$ or $\set {z \circ x, z \circ y}$ admit an infimum.
Then all three sets admit an infimum, and:
== Proof ==
First we recall that by definition of ordered group, $\preccurlyeq$ is compatible with $\circ$:
Let $\set {x, y}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {x, y}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower bounds $d$ of $\set {x, y}$ in $S$.
Thus we have:
Hence $\inf \set {x, y} \circ z$ is a lower bound of $\set {x \circ z, y \circ z}$.
Let $d$ be a lower bound of $\set {x \circ z, y \circ z}$.
Then as $G$ is a group we have that:
:$d = d' \circ z$
for some $d' \in G$.
Then:
Hence $\inf \set {x, y} \circ z$ is a lower bound of $\set {x \circ z, y \circ z}$ which is smaller than an arbitrary lower bound $d$ of $\set {x \circ z, y \circ z}$.
That is, $\inf \set {x, y} \circ z$ is an infimum of $\set {x \circ z, y \circ z}$.
Let $\set {x \circ z, y \circ z}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {x \circ z, y \circ z}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower bounds $d$ of $\set {x \circ z, y \circ z}$ in $S$.
As $G$ is a group, there exists $c' \in G$ such that $c' \circ z = c$.
Thus we have:
Hence $z \circ c'$ is a lower bound of $\set {z \circ x, z \circ y}$.
Let $d$ be a lower bound of $\set {z \circ x, z \circ y}$.
As $G$ is a group, there exists $d' \in G$ such that $z \circ d' = d$.
Then:
Hence $z \circ c'$ is a lower bound of $\set {z \circ x, z \circ y}$ which is smaller than an arbitrary lower bound $d$ of $\set {z \circ x, z \circ y}$.
That is, $z \circ c'$ is an infimum of $\set {z \circ x, z \circ y}$.
Let $\set {z \circ x, z \circ y}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {z \circ x, z \circ y}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower bounds $d$ of $\set {z \circ x, z \circ y}$ in $S$.
As $G$ is a group, there exists $c' \in G$ such that $z \circ c' = c$.
Thus we have:
Hence $c'$ is a lower bound of $\set {x, y}$.
Let $d$ be a lower bound of $\set {x, y}$.
Then:
Hence $c'$ is a lower bound of $\set {x, y}$ which is smaller than an arbitrary lower bound $d$ of $\set {x, y}$.
That is, $c'$ is an infimum of $\set {x, y}$.
Hence by definition of $c'$:
:$z \circ \inf \set {x, y} = \inf \set {z \circ x, z \circ y}$
Thus we have shown that if any of the three sets $\set {x, y}$, $\set {x \circ z, y \circ z}$ or $\set {z \circ x, z \circ y}$ admit an infimum, they all do, and:
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 15$: Ordered Semigroups: Exercise $15.10 \ \text {(b)}$
Category:Ordered Groups
Category:Infima
Infima of two Real Sets

== Theorem ==
Let $S$ and $T$ be sets of real numbers.
Let $S$ and $T$ admit infima.
Then:
: $\inf S \ge \inf T \iff \forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T: s + \epsilon > t$
== Proof ==
Let:
: $-S = \set {-s: s \in S}$
: $-T = \set {-t: t \in T}$
Observe that:
: $s \in S \iff -s \in -S$
: $t \in T \iff -t \in -T$
We know that $\inf S$ and $\inf T$ exist.
The expression $\inf S \ge \inf T$ exists as $\inf S$ and $\inf T$ exist.
In other words, for fixed sets $S$ and $T$, $\inf S \ge \inf T$ is either true or false.
We find:
=== Lemma ===
Let $X$ be a set of real numbers.
Let $X$ admit an infimum.
Let $-X = \set {-x: x \in X}$.
Then:
: $ \sup -X = -\inf X$
=== Proof ===
Because $X$ admits an infimum, it follows that it is not empty.
The result follows by Negative of Infimum is Supremum of Negatives.
== Also see ==
* Suprema of two Real Sets
Category:Real Analysis
Infimum Plus Constant

== Theorem ==
Let $T$ be a subset of the set of real numbers.
Let $T$ be bounded below.
Let $\xi \in \R$.
Then:
:$\ds \map {\inf_{x \mathop \in T} } {x + \xi} = \xi + \map {\inf_{x \mathop \in T} } x$
where $\inf$ denotes infimum.
== Proof ==
From Negative of Infimum is Supremum of Negatives, we have that:
:$\ds -\inf_{x \mathop \in T} x = \map {\sup_{x \mathop \in T} } {-x} \implies \inf_{x \mathop \in T} x = -\map {\sup_{x \mathop \in T} } {-x}$
Let $S = \set {x \in \R: -x \in T}$.
From Negative of Infimum is Supremum of Negatives, $S$ is bounded above.
We have:
== Sources ==
* : $\S 2$: Continuum Property: Exercise $\S 2.13 \ (3)$
Category:Real Analysis
Infimum Precedes Coarser Infimum

== Theorem ==
Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Let $X, Y$ be subsets of $S$ such that
:$Y$ is coarser than $X$.
Then $\inf X \preceq \inf Y$
where $\inf X$ denotes the infimum of $X$.
== Proof ==
We will prove that
:$\inf X$ is lower bound for $Y$.
Let $x \in Y$.
By definition of coarser subset:
:$\exists y \in X: y \preceq x$
By definitions of infimum and lower bound:
:$\inf X \preceq y$
Thus by definition of transitivity:
:$\inf X \preceq x$
Hence by definition of infimum:
:$\inf X \preceq \inf Y$
== Sources ==
* 
Category:Complete Lattices
Infimum and Supremum of Subgroups

== Theorem ==
Let $\struct {G, \circ}$ be a group.
Let $\mathbb G$ be the set of all subgroups of $G$.
Let $\struct {\mathbb G, \subseteq}$ be the complete lattice formed by $\mathbb G$ and $\subseteq$.
Let $H, K \in \mathbb G$.
=== Infimum of Subgroups in Lattice ===
=== Supremum of Subgroups in Lattice ===
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Theorem $14.6$
Category:Complete Lattices
Category:Subgroups
Infimum in Ordered Subset

== Theorem ==
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.
Let $X \subseteq T$ such that
:$X$ admits an infimum in $L$.
Then $\inf_L X \in T$ 
:$X$ admits an infimum in $R$ and $\inf_R X = \inf_L X$
== Proof ==
By definition of ordered subset:
:$T \subseteq S$
and
:$\forall x, y \in T: x \preceq' y \iff x \preceq y$
=== Sufficient Condition ===
Let $\inf_L X \in T$.
By definition of infimum:
:$\inf_L X$ is lower bound for $X$ in $L$.
By definition of $\preceq'$:
:$\inf_L X$ is lower bound for $X$ in $R$.
We will prove that:
:$\forall x \in T: x$ is lower bound for $X$ in $R \implies x \preceq' \inf_L X$
Let $x \in T$ such that:
:$x$ is lower bound for $X$ in $R$.
By definition of $\preceq'$:
:$x$ is lower bound for $X$ in $L$.
By definition of infimum:
:$x \preceq \inf_L X$
Thus by definition of $\preceq'$:
:$x \preceq' \inf_L X$
Hence $X$ admits an infimum in $R$ and $\inf_R X = \inf_L X$.
=== Necessary Condition ===
Assume that:
:$X$ admits an infimum in $R$ and $\inf_R X = \inf_L X$
By definition of infimum:
:$\inf_R X \in T$
Thus by assumption:
:$\inf_L X \in T$
== Sources ==
* 
Category:Ordered Sets
Category:Infima
Infimum is Product in Order Category

== Theorem ==
Let $\mathbf P$ be an order category whose ordering is $\preceq$.
Let $p, q \in \mathbf P_0$, and suppose that they have some infimum $r = \inf \set {p, q}$.
Then $r$ is a binary product of $p$ and $q$ in $\mathbf P$.
== Proof ==
Suppose that there are morphisms $l \to p$ and $l \to q$ in $\mathbf P$.
That is to say, suppose $l \preceq p$ and $l \preceq q$.
Then $l$ is a lower bound for $\set {p, q}$.
By definition of infimum, we then have:
:$l \preceq r = \inf \set {p, q}$
By definition of $\mathbf P$ as an order category, this means there is a morphism:
:$l \to r$
By definition of $\mathbf P$, this morphism is necessarily unique.
Thus $r$ satisfies the UMP for the binary product of $p$ and $q$.
The result follows.
== Also see ==
* Supremum is Coproduct in Order Category, the dual result
== Sources ==
* : $\S 2.5.4$
Category:Order Categories
Infimum is Unique

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a non-empty subset of $S$.
Then $T$ has at most one infimum in $S$.
== Proof ==
Let $c$ and $c'$ both be infima of $T$ in $S$.
From the definition of infimum, $c$ and $c'$ are lower bounds of $T$ in $S$.
By that definition:
:$c$ is a lower bound of $T$ in $S$ and $c'$ is an infimum of $T$ in $S$ implies that $c \preceq c'$
:$c'$ is a lower bound of $T$ in $S$ and $c$ is an infimum of $T$ in $S$ implies that $c' \preceq c$.
So:
:$c' \preceq c \land c \preceq c'$
and thus by the antisymmetry of the ordering $\preceq$:
:$c = c'$
== Sources ==
* : $1$: Review of some real analysis: $\S 1.1$: Real Numbers
Category:Infima
Infimum is not necessarily Smallest Element

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ admit a infimum in $S$.
Then the infimum of $T$ in $S$ is not necessarily the smallest element of $T$.
== Proof ==
== Also see ==
* Smallest Element is Infimum
== Sources ==
* : $\S 2$: Continuum Property: $\S 2.7$: Maximum and Minimum
Category:Suprema
Category:Order Theory
Category:Infimum is not necessarily Smallest Element
Infimum is not necessarily Smallest Element/Proof

== Theorem ==
== Proof ==
Let $V$ be the subset of the real numbers $\R$ defined as:
:$V := \set {x \in \R: x > 0}$
From Infimum of Subset of Real Numbers: Example 3, $V$ admits an infimum:
:$\inf V = 0$
But $V$ has no smallest element, as follows.
We note that $\inf V = 0 \notin V$.
 $x \in V$ is the smallest element of $V$.
Then $\dfrac x 2$ is also in $V$ as $\dfrac x 2 > 0$.
But $\dfrac x 2 < x$ which contradicts $x$ as being the smallest element of $V$.
Hence there can be no smallest element of $V$.
== Sources ==
* : $\S 2$: Continuum Property: $\S 2.8$: Example $\text{(iii)}$
Category:Infimum is not necessarily Smallest Element
Infimum of Bounded Below Set of Reals is in Closure

== Theorem ==
Let $\R$ be the real number line with the usual (Euclidean} metric.
Let $H \subseteq \R$ be a bounded below subset of $\R$ such that $H \ne \O$.
Let $l = \map \inf H$ be the infimum of $H$.
Then:
:$l \in \map \cl H$
where $\map \cl H$ denotes the closure of $H$ in $\R$.
== Proof ==
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {B_\epsilon} l$ be the open $\epsilon$-ball of $l$ in $\R$.
From Distance from Subset of Real Numbers:
:$\map d {l, H} = 0$
Thus by definition of distance from subset:
:$\exists x \in H: \map d {l, x} < \epsilon$
Thus $x \in \map {B_\epsilon} l$.
As $x \in H$ and $x \in \map {B_\epsilon} l$, from the definition of intersection:
:$x \in H \cap \map {B_\epsilon} l$
The result follows from Condition for Point being in Closure.
== Also see ==
* Supremum of Bounded Above Set of Reals is in Closure
== Sources ==
* : $3$: Continuity generalized: topological spaces: $3.7$: Definitions: Examples $3.7.13$
Category:Set Closures
Category:Real Number Line with Euclidean Metric
Infimum of Empty Set is Greatest Element

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Suppose that $\map \inf \O$, the infimum of the empty set, exists in $S$.
Then $\forall s \in S: s \preceq \map \inf \O$.
That is, $\map \inf \O$ is the greatest element of $S$.
== Proof ==
Observe that, vacuously, any $s \in S$ is a lower bound for $\O$.
But for any lower bound $s$ of $\O$, $s \preceq \map \inf \O$ by definition of infimum.
Hence:
:$\forall s \in S: s \preceq \map \inf \O$
== Also see ==
* Supremum of Empty Set is Smallest Element
Category:Empty Set
Category:Infima
Infimum of Image of Upper Closure of Element under Increasing Mapping

== Theorem ==
Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered set.
Let $f: S \to T$ be an increasing mapping.
Let $x \in S$.
Then $\map \inf {f \sqbrk {x^\succeq} } = \map f x$
== Proof ==
By Infimum of Upper Closure of Element:
:$\inf x^\succeq = x$
By definition of infimum:
:$x$ is lower bound for $x^\succeq$
Thus by Increasing Mapping Preserves Lower Bounds:
:$\map f x$ is lower bound for $f \sqbrk {x^\succeq}$
By definition of reflexivity:
:$x \preceq x$
By definition of upper closure of element:
:$x \in x^\succeq$
By definition of image of set:
:$\map f x \in f \sqbrk {x^\succeq}$
Thus by definition:
:$\forall y \in T: y$ is lower bound for $f \sqbrk {x^\succeq} \implies y \precsim \map f x$
Thus by definition of infimum:
:$\map \inf {f \sqbrk {x^\succeq} } = \map f x$
== Sources ==
* 
Category:Upper Closures
Infimum of Infima

== Theorem ==
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $\mathbb T$ be a collection of subsets of $S$.
Suppose all $T \in \mathbb T$ admit an infimum $\inf T$ in $S$.
Then:
:$\inf \bigcup \mathbb T = \inf \left\{{\inf T: T \in \mathbb T}\right\}$
as soon as one of these two quantities exists.
== Proof ==
Suppose that $s = \inf \bigcup \mathbb T \in S$.
By Set is Subset of Union, $T \subseteq \bigcup \mathbb T$ for all $T \in \mathbb T$.
Hence by Infimum of Subset:
:$\forall T \in \mathbb T: s \preceq \inf T$
Suppose now that $a \in S$ satisfies:
:$\forall T \in \mathbb T: a \preceq \inf T$
Then by transitivity of $\preceq$:
:$\forall t \in T: a \preceq t$
Since this holds for any $T \in \mathbb T$, also:
:$\forall t \in \bigcup \mathbb T: a \preceq t$
Hence $a \preceq s$, by definition of infimum.
That is, $s = \inf \left\{{\inf T: T \in \mathbb T}\right\}$.
Suppose now that $r = \inf \left\{{\inf T: T \in \mathbb T}\right\} \in S$.
By definition of infimum, for all $T \in \mathbb T$ and $t \in T$:
:$\inf T \preceq t$
By transitivity of $\preceq$:
:$\forall T \in \mathbb T: \forall t \in T: r \preceq t$
Hence for all $t \in \bigcup \mathbb T$:
:$r \preceq t$
Suppose that $a \in S$ satisfies:
:$\forall t \in \bigcup \mathbb T: a \preceq t$
In particular, for any $T \in \mathbb T$, since $T \subseteq \bigcup \mathbb T$:
:$a \preceq \inf T$
and therefore by definition of infimum, also:
:$a \preceq r$
That is, $r = \inf \bigcup \mathbb T$.
Category:Order Theory
Infimum of Intersection of Upper Closures equals Join Operands

== Theorem ==
Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x, y \in S$.
Then $\map \inf {x^\succeq \cap y^\succeq} = x \vee y$
== Proof ==
By Intersection of Upper Closures is Upper Closure of Join Operands:
:$x^\succeq \cap y^\succeq = \paren {x \vee y}^\succeq$
Thus by Infimum of Upper Closure of Element:
:$\map \inf {x^\succeq \cap y^\succeq} = x \vee y$
== Sources ==
* 
Category:Upper Closures
Infimum of Open Set is Way Below Element in Complete Scott Topological Lattice

== Theorem ==
Let $T = \struct {S, \preceq, \tau}$ be a complete topological lattice with Scott topology.
Let $X$ be an open subset of $S$,
Let $x \in X$.
Then $\inf X \ll x$
where $\ll$ denotes the way below relation.
== Proof ==
By Open iff Upper and with Property (S) in Scott Topological Lattice:
:$X$ is upper and has property (S).
Let $D$ be a directed subset of $S$ such that
:$x \preceq \sup D$
By definition of upper section:
:$\sup D \in X$
By definition of property (S):
:$\exists y \in D: \forall d \in D: y \preceq d \implies d \in X$
By definitions of infimum and complete lattice:
:$\inf X$ is a lower bound for $X$.
By definition pf reflexivity:
:$y \in X$
Thus by definition of lower bound:
:$\exists d \in D: \inf X \preceq d$
Thus by definition pf way below relation:
:$\inf X \ll x$
== Sources ==
* 
* 
Category:Topological Order Theory
Category:Way Below Relation
Infimum of Power Set

== Theorem ==
Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the relational structure defined on $\powerset S$ by the relation $\subseteq$.
(From Subset Relation on Power Set is Partial Ordering, this is an ordered set.)
Then the infimum of $\struct {\powerset S, \subseteq}$ is the empty set $\O$.
== Proof ==
Follows directly from Empty Set is Subset of All Sets and the definition of infimum.
Category:Power Set
Category:Empty Set
Category:Order Theory
Infimum of Real Subset

== Lemma ==
Let $S$ be a set of extended real numbers.
Let $S$ be bounded below in $\R$.
Let $T = S \cap \R$.
Then:
:$S$ admits an infimum in $\R$ $T$ admits an infimum in $\R$
and, if $\inf S$ and $\inf T$ exist as real numbers:
:$\inf S = \inf T$
== Proof ==
We observe that $T$ constitutes the real numbers of $S$.
Since there is a real number that is a lower bound for $S$, $-\infty$ is not an element of $S$.
Accordingly, $\infty$ is the only possible element of $S \setminus T$.
Therefore:
:$S$ is a subset of $T \cup \set \infty$
First, we show that $S$ and $T$ have the same set of lower bounds.
Let $b$ be a lower bound in $\R$ for $S$.
Then $b$ is a lower bound for $T$ as $T$ is a subset of $S$.
Therefore:
:the set of lower bounds for $S$ is a subset of the set of lower bounds for $T$
Assume that $c$ is a lower bound in $\R$ for $T$.
Then $c$ is a lower bound for $T \cup \set \infty$ as well since $c < \infty$.
Accordingly, $c$ is a lower bound for $S$ since $S$ is a subset of $T \cup \set \infty$.
Therefore:
:the set of lower bounds for $T$ is a subset of the set of lower bounds for $S$
We have:
:the set of lower bounds for $T$ is a subset of the set of lower bounds for $S$
:the set of lower bounds for $S$ is a subset of the set of lower bounds for $T$
Therefore:
:the set of lower bounds for $T$ equals the set of lower bounds for $S$ by definition
Next, we show that $S$ and $T$ have the same infima.
We have that $S$ and $T$ have the same set of lower bounds.
Therefore, $S$ and $T$ have the same greatest lower bound in $\overline \R$.
Accordingly, as a corollary, if one of the sets $S$ and $T$ admits an infimum in $\R$, so does the other.
Furthermore, these infima are equal.
Category:Extended Real Numbers‎
Infimum of Set of Integers equals Smallest Element

== Theorem ==
Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded below in the set of real numbers $\R$.
Then $S$ has a smallest element, and it is equal to the infimum $\sup S$.
== Proof ==
By Set of Integers Bounded Below by Real Number has Smallest Element, $S$ has a smallest element, say $n \in S$.
By Smallest Element is Infimum, $n$ is the infimum of $S$.
== Also see ==
* Supremum of Set of Integers equals Greatest Element
* Infimum of Set of Integers is Integer
* Infimum is Unique
Category:Integers
Infimum of Set of Integers is Integer

== Theorem ==
Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded below in the set of real numbers.
Then its infimum $\inf S$ is an integer.
== Proof ==
By Infimum of Set of Integers equals Smallest Element, $S$ has a smallest element $n \in \Z$, that is equals to the infimum of $S$.
== Also see ==
* Supremum of Set of Integers is Integer
* Infimum is Unique
Category:Integers