English
Let S be a subset of a semilattice with infimum. The set of all pairwise infima S ⊼ S equals S if and only if S is closed under infimum (InfClosed).
Русский
Пусть S ⊆ α, где α — полулинейное полукольцо с операцией inf. Тогда множество всех инфимумов пар элементов из S равняется S тогда и только тогда, когда S замкнуто относительно инфимума (InfClosed(S)).
LaTeX
$$$\\{ a \\in \\alpha \\mid \\exists x,y \\in s,\; a = x \\wedge y \\} = s \\;\\Longleftrightarrow\\; \\operatorname{InfClosed}(s)$$$
Lean4
@[simp]
theorem infs_self : s ⊼ s = s ↔ InfClosed s :=
subset_infs_self.le.ge_iff_eq'.symm.trans infs_self_subset
