English
Finite sets form a lattice under union and intersection, with join = union and meet = intersection.
Русский
Конечные множества образуют решётку относительно объединения и пересечения, где наибольшее верхнее объединение совпадает с объединением, а наименьшее нижнее — с пересечением.
LaTeX
$$$\\text{Finset }\\alpha \\text{ is a lattice with } s \\lor t = s \\cup t,\\; s \\land t = s \\cap t$$$
Lean4
instance : Lattice (Finset α) :=
{ Finset.partialOrder with
sup := (· ∪ ·)
sup_le := fun _ _ _ hs ht _ ha => (mem_ndunion.1 ha).elim (fun h => hs h) fun h => ht h
le_sup_left := fun _ _ _ h => mem_ndunion.2 <| Or.inl h
le_sup_right := fun _ _ _ h => mem_ndunion.2 <| Or.inr h
inf := (· ∩ ·)
le_inf := fun _ _ _ ht hu _ h => mem_ndinter.2 ⟨ht h, hu h⟩
inf_le_left := fun _ _ _ h => (mem_ndinter.1 h).1
inf_le_right := fun _ _ _ h => (mem_ndinter.1 h).2 }
