instDistribLattice — Mathlib

English

Finite sets form a distributive lattice under union and intersection.

Русский

Конечные множества образуют распределённую решётку относительно объединения и пересечения.

LaTeX

$$$\operatorname{DistribLattice}(\operatorname{Finset}(\alpha))$$$

Lean4

instance : DistribLattice (Finset α) :=
  {
    le_sup_inf := fun a b c => by
      simp +contextual only [sup_eq_union, inf_eq_inter, le_eq_subset, subset_iff, mem_inter, mem_union, and_imp,
        or_imp, true_or, imp_true_iff, true_and, or_true] }

Похожие утверждения