English
Let α be a semilattice with infimum ⊓ and bottom ⊥. Let s ⊆ ι and f: ι → α. If the family (f i) for i ∈ s is pairwise disjoint, and each f i (with i ∈ s) is not equal to ⊥, and whenever i, j ∈ s satisfy f i ≤ f j, then i = j.
Русский
Пусть α — полупорядоченное множество с наибольшим низшим пределом ⊓ и нижней границей ⊥. Пусть s ⊆ ι и f: ι → α. Если семейство (f i) для i ∈ s попарно непересекается, и каждое f i для i ∈ s не равно ⊥, а при i, j ∈ s выполняется f i ≤ f j, то i = j.
LaTeX
$$$$\text{Let } \alpha \text{ be a semilattice with infimum and bottom } s \subseteq \iota, \ f: \iota \to \alpha. \\ s.{\text{PairwiseDisjoint}}(f) \ \text{and} \ \forall i \in s, f(i) \neq \bot, \ \forall i,j \in s,\ f(i) \le f(j) \Rightarrow i=j.$$$$
Lean4
theorem eq_of_le (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hf : f i ≠ ⊥) (hij : f i ≤ f j) :
i = j :=
(hs.elim' hi hj) fun h => hf <| (inf_of_le_left hij).symm.trans h
