English
The family Set α forms a distributive lattice under inclusion, with join given by union and meet by intersection.
Русский
Тогда множество подмножеств α образуют распределённую решётку по включению: объединение служит верхой операцией, пересечение — нижней.
LaTeX
$$\\text{Set }\\alpha \\\\text{ is a distributive lattice with } \\sup = \\cup, \\inf = \\cap, \\\\ top = \\univ, \\bot = \\varnothing$$
Lean4
instance instDistribLattice : DistribLattice (Set α)
where
__ : DistribLattice (α → Prop) := inferInstance
le := (· ≤ ·)
lt := fun s t => s ⊆ t ∧ ¬t ⊆ s
sup := (· ∪ ·)
inf := (· ∩ ·)