nyuuzyou/wikis huggingface dataset:
Meet-Continuous and Distributive implies Shift Mapping Preserves Finite Suprema

== Theorem ==
Let $\struct {S, \vee, \wedge, \preceq}$ be a meet-continuous distributive complete lattice.
Let $x \in S$.
Let $f: S \to S$ be a mapping such that
:$\forall y \in S: \map f y = x \wedge y$
Then
:$f$ preserves finite suprema
== Proof ==
Let $X$ be finite subset of $S$ such that:
:$X$ admits a supremum
By definition of complete lattice:
:$f \sqbrk X$ admits a supremum
We will prove the result by induction on the cardinality of $X$.
=== Basis Case ===
:$\forall X \subseteq S: \card X = 0 \implies \map \sup {f \sqbrk X} = \map f {\sup X}$
where:
:$\card X$ denotes the cardinality of $X$
Let $X \subseteq S$ such that:
:$\card X = 0$
By Cardinality of Empty Set:
:$X = \O$
By definition of image of set:
:$f \sqbrk X = \O$
By definitions of bottom and smallest element:
:$\bot \preceq x$
Thus:
=== Induction Hypothesis ===
:$\forall X \subseteq S: \card X = n \implies \map \sup {f \sqbrk X} = \map f {\sup X}$
=== Induction Step ===
:$\forall X \subseteq S: \card X = n + 1 \implies \map \sup {f \sqbrk X} = \map f {\sup X}$
Let $X \subseteq S$ such that:
:$\card X = n + 1$
Then $X = \set {x_1, \dots, x_n, x_{n + 1} }$.
Thus:
== Sources ==
* 
* 
Category:Distributive Lattices
Category:Meet-Continuous Lattices
Category:Complete Lattices
Meet-Continuous iff Ideal Supremum is Meet Preserving

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Let $f: \map {\it Ids} {\mathscr S} \to S$ be a mapping such that:
:$\forall I \in \map {\it Ids} {\mathscr S}: \map f I = \sup_{\mathscr S} I$
where 
:$\map {\it Ids} {\mathscr S}$ denotes the set of all ideals in $\mathscr S$
Then
:$\mathscr S$ is meet-continuous
:$f$ preserves meet as a mapping from $\struct {\map {\it Ids} {\mathscr S}, \subseteq}$ into $\mathscr S$
== Proof ==
=== Sufficient Condition ===
Let $\mathscr S$ be meet-continuous.
We will prove that:
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
Let $D_1, D_2$ be directed subsets of $S$.
we will prove as sublemma that:
:for every an element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x = \sup \set {x \wedge d: d \in D}$
Let $x \in S$, $D$ be a directed subset of $S$ such that:
:$x \preceq \sup D$
Thus:
By definition of reflexivity:
:for every element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x \preceq \sup \set {x \wedge d: d \in D}$
Define a mapping $g: S \times S \to S$:
:$\forall \tuple {s, t} \in S \times S: \map g {s, t} = s \wedge t$
By Meet is Directed Suprema Preserving:
:$g$ preserves directed suprema as a mapping from the simple order product $\struct {S \times S, \precsim}$ of $\mathscr S$ and $\mathscr S$ into $\mathscr S$.
Thus by Meet is Directed Suprema Preserving implies Meet of Suprema equals Supremum of Meet of Directed Subsets: 
:$\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
By exemplification:
:for every ideals $I_1, I_2$ of $S$: $\paren {\sup I_1} \wedge \paren {\sup I_2} = \sup \set {d_1 \wedge d_2: d_1 \in I_1, d_2 \in I_2}$
Thus by Meet of Suprema equals Supremum of Meet of Ideals implies Ideal Supremum is Meet Preserving:
:$f$ preserves meet.
=== Necessary Condition ===
Let $f$ be such that it preserves meet.
Thus:
:$\mathscr S$ is up-complete
We will prove that:
:for every ideals $I_1, I_2$ in $\mathscr S$: $\paren {\sup I_1} \wedge \paren {\sup I_2} = \sup \set {i_1 \wedge i_2: i_1 \in I_1, i_2 \in I_2}$
Let $I_1, I_2$ be ideals in $\mathscr S$.
Thus:
We will prove that:
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
Let $D_1, D_2$ be directed subsets of $S$.
By definition of up-complete:
:$D_1$ and $D_2$ admit suprema
By Supremum of Lower Closure of Set:
:$D_1^\preceq$ and $D_2^\preceq$ admit suprema
Thus:
It remains to prove (MC) of definition of meet-continuous.
Let $x$ be an element of $S$.
Let $D$ be a directed subset of $S$.
By Singleton is Directed and Filtered Subset:
:$\set x$ is directed.
Thus:
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Meet-Continuous iff Meet Preserves Directed Suprema

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Let $\struct {S \times S, \precsim}$ be the simple order product of $\mathscr S$ and $\mathscr S$.
Let $f: S \times S \to S$ be a mapping such that
:$\forall x, y \in S: \map f {x, y} = x \wedge y$
Then:
:$\mathscr S$ is meet-continuous
:
:$f$ preserves directed suprema
== Proof ==
=== Sufficient Condition ===
Assume that:
:$\mathscr S$ is meet-continuous.
We will prove that:
:for every element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x = \sup \set {x \wedge d: d \in D}$
Let $x \in S$, $D$ be a directed subset of $S$ such that:
:$x \preceq \sup D$
Thus
By definition of reflexivity:
:for every an element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x \preceq \sup \set {x \wedge d: d \in D}$
By Meet is Directed Suprema Preserving:
:$f$ preserves directed suprema.
=== Necessary Condition ===
Assume that:
:$f$ preserves directed suprema.
By Meet is Directed Suprema Preserving implies Meet of Suprema equals Supremum of Meet of Directed Subsets: 
:$\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
Thus by Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Directed Subsets:
:$\mathscr S$ is meet-continuous.
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Directed Subsets

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Then:
:$\mathscr S$ is meet-continuous
:
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
== Proof ==
=== Sufficient Condition ===
Let $\mathscr S$ be meet-continuous.
By Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Ideals:
:for every ideals $I, J$ in $\mathscr S$: $\paren {\sup I} \wedge \paren {\sup J} = \sup \set {i \wedge j: i \in I, j \in J}$
Let $D_1, D_2$ directed subsets of $S$.
By definition of up-complete:
:$D_1$ and $D_2$ admit suprema
By Supremum of Lower Closure of Set:
:$D_1^\preceq$ and $D_2^\preceq$ admit suprema
where
:$D_1^\preceq$ denotes the lower closure of $D_1$.
Thus
=== Necessary Condition ===
Assume that
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
By exemplification:
:for every ideals $I_1, I_2$ of $S$: $\paren {\sup I_1} \wedge \paren {\sup I_2} = \sup \set {d_1 \wedge d_2: d_1 \in I_1, d_2 \in I_2}$
Thus by Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Ideals:
:$\mathscr S$ is meet-continuous.
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Ideals

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Then
:$\mathscr S$ is meet-continuous 
:for every ideals $I, J$ in $\mathscr S$: $\paren {\sup I} \wedge \paren {\sup J} = \sup \set {i \wedge j: i \in I, j \in J}$
== Proof ==
=== Sufficient Condition ===
Let $\mathscr S$ be meet-continuous.
Define $\II$, the set of all ideals in $\mathscr S$
Define a mapping $f: \II \to S$ such that
:$\forall I \in \II: \map f I = \sup I$
By Meet-Continuous iff Ideal Supremum is Meet Preserving:
:$f$ preserves meet.
Let $I, J \in \II$.
By definition of mapping preserves meet:
:$f$ preserves the infimum of $\set {I, J}$
Thus
=== Necessary Condition ===
Assume that for every ideals $I, J$ in $\mathscr S$:
:$\paren {\sup I} \wedge \paren {\sup J} = \sup \set {i \wedge j: i \in I, j \in J}$
By Meet of Suprema equals Supremum of Meet of Ideals implies Ideal Supremum is Meet Preserving:
:$f$ preserves meet.
Thus by Meet-Continuous iff Ideal Supremum is Meet Preserving:
:$\mathscr S$ is meet-continuous.
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Meet-Continuous iff if Element Precedes Supremum of Directed Subset then Element equals Supremum of Meet of Element by Directed Subset

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Then
:$L$ is meet-continuous
:
:$\forall x \in S$, the directed subset $D$ of $S: x \preceq \sup D \implies x = \sup \set {x \wedge d: d \in D}$
== Proof ==
=== Sufficient Condition ===
Let $L$ be meet-continuous.
Let $x$ be an element of $S$, $D$ be a directed subset of $S$ such that
:$x \preceq \sup D$
Thus
=== Necessary Condition ===
Let:
:$\forall x \in S$, directed subset $D$ of $S: x \preceq \sup D \implies x = \sup \set {x \wedge d: d \in D}$
By definition of reflexivity:
:$\forall x \in S$, directed subset $D$ of $S: x \preceq \sup D \implies x \preceq \sup \set {x \wedge d: d \in D}$
By Meet is Directed Suprema Preserving:
:$\wedge$ preserves directed suprema as a mapping from the simple order product $\struct {S \times S, \precsim}$ of $L$ and $L$ into $L$.
Thus by Meet-Continuous iff Meet Preserves Directed Suprema
:$L$ is meet-continuous.
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Meet-Continuous implies Shift Mapping Preserves Directed Suprema

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be a meet-continuous lattice.
Let $x \in S$.
Let $f: S \to S$ be a mapping such that:
:$\forall y \in S: \map f y = x \wedge y$
Then:
:$f$ preserves directed suprema.
== Proof ==
Let $D$ be a directed subset of $S$ such that
:$D$ admits a supremum.
By Singleton is Directed and Filtered Subset:
:$\set x$ is directed.
By Up-Complete Product/Lemma 1:
:$\set x \times D$ is directed in the simple order product $\struct {S \times S, \precsim}$ of $\mathscr S$ and $\mathscr S$.
Define a mapping $g: S \times S \to S$:
:$\forall s, t \in S: \map g {s, t} = s \wedge t$
By Meet-Continuous iff Meet Preserves Directed Suprema:
:$g$ preserves directed suprema.
By definition of meet-continuous:
:$\mathscr S$ is up-complete.
By Up-Complete Product:
:$\struct {S \times S, \precsim}$ is up-complete.
By definition of up-complete:
:$\set x \times D$ admits a supremum.
Thus
== Sources ==
* 
* 
Category:Meet-Continuous Lattices
Category:Suprema
Meet-Irreducible Open Set Induces Completely Prime Filter

== Theorem ==
Let $\struct{S, \tau}$ be a topological space.
Let:
:$W \in \tau : W \ne S : W$ is meet-irreducible
Let:
:$\FF = \set{U \in \tau : U \nsubseteq W}$.
Then:
:$\FF$ is a completely prime filter in the complete lattice $\struct{\tau, \subseteq}$
== Proof ==
=== $\FF$ satisfies ===
We have :
:$W \ne S$
From :
:$S \in \tau$
By definition of $\FF$:
:$S \in \FF$
By definition of empty set:
:$\FF \ne \O$
It follows that $\FF$ satisfies .
=== $\FF$ satisfies ===
Let $U, V \in \FF$.
By definition of $\FF$:
:$U \nsubseteq W$ and $V \nsubseteq W$
From the contrapositive statement of Characterization of Meet-Irreducible Open Set:
:$U \cap V \nsubseteq W$
By definition of $\FF$:
:$U \cap V \in \FF$
From Intersection is Subset:
:$U \cap V \subseteq U$ and $U \cap V \subseteq V$
It follows that $\FF$ satisfies .
=== $\FF$ satisfies ===
Let $U \in \FF$.
Let $V \in \tau$ such that $U \subseteq V$.
From the contrapositive statement of Subset Relation is Transitive:
:$V \nsubseteq W$
By definition of $\FF$:
:$V \in \FF$
It follows that $\FF$ satisfies .
=== $\FF$ is Proper ===
We have :
:$W \in \tau$
From Set is Subset of Itself:
:$W \notin \FF$
Hence:
:$\FF \ne \tau$
It follows that $\FF$ is a proper subset of $\tau$ by definition. 
=== $\FF$ satisfies Complete Primeness ===
Let $\VV \subseteq \tau$:
:$\bigcup \VV \in \FF$
By definition of $\FF$:
:$\bigcup \VV \nsubseteq W$
By definition of subset:
:$\exists x \in \bigcup \VV : x \notin W$
By definition of set union:
:$\exists V \in \VV : x \in V$
By definition of subset:
:$\exists V \in \VV : V \nsubseteq W$
It has been shown that $\FF$ is a completely prime filter by definition.
== Also see ==
* Topology forms Complete Lattice
Category:Meet-Irreducible Open Sets
Category:Completely Prime Filters
Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$.
Let $F = S \setminus U$.
Then:
:$U$ is a meet-irreducible open set $F$ is a closed irreducible subspace
== Proof ==
We prove the contrapositive statement:
:$F$ is not a closed irreducible subspace $U$ is not a meet-irreducible open set
=== Necessary Condition ===
Let $F$ not be a closed irreducible subspace.
=== Sufficient Condition ===
Let $U$ not be a meet-irreducible open set.
Category:Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace
Category:Meet-Irreducible Open Sets
Category:Irreducible Spaces
Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace/Necessary Condition

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$.
Let $F = S \setminus U$.
Let $F$ be a closed irreducible subspace.
Then:
:$U$ is a meet-irreducible open set
== Proof ==
By definition of closed set:
:$F$ is a closed set
By definition of closed irreducible subspace there exists proper closed subsets $F_1, F_2$ of $F$:
:$F = F_1 \cup F_2$
:$F_1 \subsetneq F$
:$F_2 \subsetneq F$
From Set Complement inverts Subsets and Equal Relative Complements iff Equal Subsets:
:$S \setminus F \subsetneq S \setminus F_1$
:$S \setminus F \subsetneq S \setminus F_2$
From De Morgan's Laws (Set Theory):
:$S \setminus F = S \setminus F_1 \cap S \setminus F_2$
Consider:
:$U_1 = S \setminus F_1$
:$U_2 = S \setminus F_2$
From Complement of Closed Set is Open Set:
:$U_1, U_2 \in \tau$
We have:
:$U \subsetneq U_1$
:$U \subsetneq U_2$
:$U = U_1 \cap U_2$
Hence:
:$U_1 \nsubseteq U$
:$U_2 \nsubseteq U$
:$U = U_1 \cap U_2$
From Characterization of Meet-Irreducible Open Set $U$ is not a meet-irreducible open set.
Category:Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace
Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace/Sufficient Condition

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$ not be a meet-irreducible open set.
Let $F = S \setminus U$.
Then:
:$F$ is not a closed irreducible subspace
== Proof ==
From Characterization of Meet-Irreducible Open Set there exists $V_1, V_2\in \tau$:
:$V_1 \nsubseteq U$
:$V_2 \nsubseteq U$
:$V_1 \cap V_2 \subseteq U$
Let:
:$U_1 = V_1 \cup U$
:$U_2 = V_2 \cup U$
From :
:$U_1, U_2 \in \tau$
From Set is Subset of Union:
:$U \subsetneq U_1$
:$U \subsetneq U_2$
We have:
From Set Complement inverts Subsets and Equal Relative Complements iff Equal Subsets:
:$S \setminus U_1 \subsetneq S \setminus U$
:$S \setminus U_2 \subsetneq S \setminus U$
From De Morgan's Laws (Set Theory):
:$S \setminus U = S \setminus U_1 \cup S \setminus U_2$
Consider:
:$F_1 = S \setminus U_1$
:$F_2 = S \setminus U_2$
By definition of closed set:
:$F_1, F_2$ and $F$ are closed sets
We have:
:$F_1 \subsetneq F$
:$F_2 \subsetneq F$
:$F_1 \cup F_2 = F$
It follows that $F$ is not a closed irreducible subspace by definition.
Category:Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace
Meet Absorbs Join

== Theorem ==
Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $\wedge$ denote meet.
Then $\wedge$ absorbs $\vee$.
That is, for all $a, b \in S$:
:$a \wedge \paren {a \vee b} = a$
== Proof ==
By Dual Pairs (Order Theory), we observe that the theorem statement is dual to that of Join Absorbs Meet.
The result follows by the Global Duality Principle.
== Duality ==
The dual to this theorem is Join Absorbs Meet.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Exercise $14.23 \ \text {(a)}$
Category:Join and Meet
Category:Absorption Laws
Meet Irreducible Element Induced by Completely Prime Filter

== Theorem ==
Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\top$ denote the greatest element of $L$.
Let $p$ be a completely prime filter of $L$.
Let:
:$b = \bigvee \set{a \in L : a \notin p}$
where:
:$\bigvee \set{a \in L : a \notin p}$ denotes the supremum of the set $\set{a \in L : a \notin p}$
Then:
:$b$ is a meet irreducible element not equal to $\top$
== Proof ==
Let: 
:$x, y \in S : x \wedge y = b$
By definition of infimum:
:$b \preceq x$
:$b \preceq y$
By the contrapositive statement of the definition of completely prime filter:
:$b \notin p$
By the contrapositive statement of filter axiom $(2)$:
:either $x \notin p$ or $y \notin p$
By definition of supremum:
:either $x \preceq b$ or $y \preceq b$
By ordering axiom $(3)$:
:either $x = b$ or $y = b$
The result follows by definition of meet irreducible element.
Category:Completely Prime Filters
Category:Meet Irreducible Elements
Meet Irreducible Induced by Completely Prime Filter Induced by Meet Irreducible

== Theorem ==
Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\top$ denote the greatest element of $L$.
For every meet-irreducible element $b$ of $L$ not equal to $\top$, let:
:$p_b = \set{a \in L : a \npreceq b}$
where
:$p_b$ is a completely prime filter of $L$.
For every completely prime filter $p$ of $L$, let:
:$b_p = \bigvee \set{a \in L : a \notin p}$
where:
:$\bigvee \set{a \in L : a \notin p}$ denotes the supremum of the set $\set{a \in L : a \notin p}$
which is a meet irreducible element not equal to $\top$
Let $b$ be a meet-irreducible element of $L$ not equal to $\top$.
Then:
:$b_{p_b} = b$
== Proof ==
We have:
Category:Completely Prime Filters
Category:Meet Irreducible Elements
Meet Irreducible iff Finite Infimum equals Element

== Theorem ==
Let $L = \left({S, \wedge, \preceq}\right)$ be a meet semilattice.
Let $x \in S$.
Then
:$x$ is meet irreducible
:for every non-empty finite subset $A$ of $S$: $x = \inf A \implies x \in A$
== Proof ==
=== Sufficient Condition ===
Let $x$ be meet irreducible.
We will prove the result by induction on cardinality of $A$.
==== Base case ====
:for every non-empty subset $A$ of $S$: $\left\vert{A}\right\vert = 1 \land x = \inf A \implies x \in A$
Let $A$ be a non-empty subset of $S$ such that
:$\left\vert{A}\right\vert = 1 \land x = \inf A$
Then
:$A = \left\{ {a}\right\}$
By Infimum of Singleton:
:$x = a$
Thus by definition of singleton:
:$x \in A$
==== Induction Hypothesis ====
:$n \ge 1$ and for every non-empty subset $A$ of $S$: $\left\vert{A}\right\vert = n \land x = \inf A \implies x \in A$
==== Induction Step ====
:$n \ge 1$ and for every non-empty subset $A$ of $S$: $\left\vert{A}\right\vert = n+1 \land x = \inf A \implies x \in A$
Let $A$ be a non-empty subset of $S$ such that
:$\left\vert{A}\right\vert = n+1 \land x = \inf A$
Then
:$A = \left\{ {a_1, \dots, a_n, a_{n+1} }\right\}$
By definition of infimum:
:$\inf A = \left({a_1 \wedge \dots \wedge a_n}\right) \wedge a_{n+1}$
By definition of meet irreducible:
:$x = a_1 \wedge \dots \wedge a_n$ or $x = a_{n+1}$
By Induction Hypothesis:
:$x \in \left\{ {a_1, \dots, a_n}\right\}$ or $x = a_{n+1}$
Thus by definition of unordered tuple:
:$x \in A$
=== Necessary Condition ===
Assume that
:for every non-empty finite subset $A$ of $S$: $x = \inf A \implies x \in A$
Let $y, z \in S$ such that
:$x = y \wedge z$
By definition of meet:
:$x = \inf \left\{ {y, z}\right\}$
By assumption:
:$x \in \left\{ {y, z}\right\}$
Thus by definition of unordered tuple:
:$x = y$ or $x = z$
== Sources ==
* 
* 
Category:Order Theory
Category:Meet Irreducible Elements
Meet Precedes Operands

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $a, b \in S$ admit a meet $a \wedge b \in S$.
Then:
:$a \wedge b \preceq a$
:$a \wedge b \preceq b$
That is, $a \wedge b$ precedes its operands $a$ and $b$.
== Proof ==
By definition of meet:
:$a \wedge b = \inf \set {a, b}$
where $\inf$ denotes infimum.
Since an infimum is a lower bound:
:$\inf \set {a, b} \preceq a$
:$\inf \set {a, b} \preceq b$
as desired.
Category:Meet Operation
Meet Preserves Directed Suprema/Lemma 2

== Theorem ==
Let $x$ be an element of $S$, $D$ be a directed subset of $S$.
Then:
:$\paren {\sup D} \wedge x = \sup \set {d \wedge x: d \in D}$
== Proof ==
By Meet Precedes Operands:
:$\paren {\sup D} \wedge x \preceq \sup D$
By assumption:
:$\paren {\sup D} \wedge x \preceq \sup \set {\paren {\sup D} \wedge x \wedge d: d \in D}$
By definition of supremum:
:$\forall d \in D: d \preceq \sup D$
By Preceding iff Meet equals Less Operand:
:$\forall d \in D: d \wedge \sup D = d$
By Meet is Associative and Meet is Commutative:
:$\paren {\sup D} \wedge x \preceq \sup \set {d \wedge x: d \in D}$
By Meet Semilattice is Ordered Structure:
:$\forall d \in D: d \wedge x \preceq \paren {\sup D} \wedge x$
By definition:
:$\paren {\sup D} \wedge x$ is upper bound for $\set {d \wedge x: d \in D}$
By definition of supremum:
:$\sup \set {d \wedge x: d \in D} \preceq \paren {\sup D} \wedge x$
if $\set {d \wedge x: d \in D}$ admits a supremum
We will prove that:
:$\set {d \wedge x: d \in D}$ is directed
Let $y, z \in \set {d \wedge x: d \in D}$.
Then
:$\exists d_1 \in D: y = d_1 \wedge x$
and
:$\exists d_2 \in D: z = d_2 \wedge x$
By definition of directed subset:
:$\exists d \in D: d_1 \preceq d \land d_2 \preceq d$
By Meet Semilattice is Ordered Structure:
:$y \preceq d \wedge x$ and $z \preceq d \wedge x$
Thus
:$d \wedge x \in \set {d \wedge x: d \in D}$
Hence by definition:
:$\set {d \wedge x: d \in D}$ is directed.
By definition of up-complete:
:$\set {d \wedge x: d \in D}$ admits a supremum
Thus by definition of antisymmetry:
:$\paren {\sup D} \wedge x = \sup \set {d \wedge x: d \in D}$
== Sources ==
* 
* 
Category:Up-Complete Semilattices
Meet Semilattice Filter iff Ordered Set Filter

== Theorem ==
Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $F \subseteq S$ be a non-empty subset of $S$.
Then:
:$F$ is a meet semilattice filter of $\struct {S, \wedge, \preceq}$ $F$ is an ordered set filter of $\struct {S, \preceq}$.
== Proof ==
=== Necessary Condition ===
Let $F$ be a meet semilattice filter of $\struct {S, \wedge, \preceq}$.
To show that $F$ is an ordered set filter of $\struct {S, \preceq}$ it is sufficient to show:
Let $x, y \in F$.
Let $z = x \wedge y$.
By definition of meet semilattice filter, $F$ is a subsemilattice, so:
:$z \in F$
By definition of Meet:
:$z \preceq x \text{ and } z \preceq y$
The result follows.
=== Sufficient Condition ===
Let $F$ be an ordered set filter of $\struct {S, \preceq}$.
To show that $F$ is a meet semilattice filter of $\struct {S, \wedge, \preceq}$ it is sufficient to show:
Let $x, y \in F$.
By definition of ordered set filter:
:$\exists z \in F : z \preceq x \text { and } z \preceq y$
By definition of meet:
:$z \preceq x \wedge y$
By definition of ordered set filter:
:$x \wedge y \in F$
The result follows.
Category:Meet Semilattices
Meet Semilattice has Greatest Element iff has Identity

== Theorem ==
Let $\struct{S, \wedge, \preceq}$ be a meet semilattice.
Let $s \in S$.
Then:
:$s$ is the greatest element of $S$
:$s$ is the identity in $\struct{S, \wedge}$.
== Proof ==
This is the dual statement of Join Semilattice has Smallest Element iff has Identity by Dual Pairs (Order Theory).
The result follows from the Duality Principle.
Category:Meet Semilattices
Meet Semilattice is Ordered Structure

== Theorem ==
Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Then $\struct {S, \wedge, \preceq}$ is an ordered structure.
== Proof ==
For $\struct {S, \wedge, \preceq}$ to be an ordered structure is equivalent to, for all $a,b,c \in S$:
:$a \preceq b \implies a \wedge c \preceq b \wedge c$
:$a \preceq b \implies c \wedge a \preceq c \wedge b$
Since Meet is Commutative, it suffices to prove the first of these implications.
By definition of meet:
:$b \wedge c = \inf \set {b, c}$
where $\inf$ denotes infimum.
By Meet Precedes Operands:
:$a \wedge c \preceq a$
:$a \wedge c \preceq c$
Now also $a \preceq b$, and by transitivity of $\preceq$ we find that:
:$a \wedge c \preceq b$
Thus $a \wedge c$ is a lower bound for $\set {b, c}$.
Hence:
:$a \wedge c \preceq b \wedge c$
by definition of infimum.
== Also see ==
* Join Semilattice is Ordered Structure
Category:Meet Semilattices
Category:Ordered Structures