instDistribLattice — Mathlib

English

The collection of filters on α forms a distributive lattice under the usual join and inf operations.

Русский

Множество фильтров на α образует распределительную решётку по операциям объединения и наименьшего верхнего предела.

LaTeX

$$DistribLattice (Filter α)$$

Lean4

instance : DistribLattice (Filter α) :=
  { Filter.instCompleteLatticeFilter with
    le_sup_inf := by
      intro x y z s
      simp only [and_assoc, mem_inf_iff, mem_sup, exists_imp, and_imp]
      rintro hs t₁ ht₁ t₂ ht₂ rfl
      exact ⟨t₁, x.sets_of_superset hs inter_subset_left, ht₁, t₂, x.sets_of_superset hs inter_subset_right, ht₂, rfl⟩ }

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