instCompleteLatticeFilter — Mathlib

English

Filter α forms a complete lattice under the usual order, with infimum and supremum given by the standard operations.

Русский

Фильтры на α образуют полную решётку относительно обычного порядка, где inf и sup соответствуют стандартным операциям.

LaTeX

$$$\\text{CompleteLattice}(\\mathrm{Filter}(\\alpha))$$$

Lean4

/-- Complete lattice structure on `Filter α`. -/
instance instCompleteLatticeFilter : CompleteLattice (Filter α)
    where
  inf a b := min a b
  sup a b := max a b
  le_sup_left _ _ _ h := h.1
  le_sup_right _ _ _ h := h.2
  sup_le _ _ _ h₁ h₂ _ h := ⟨h₁ h, h₂ h⟩
  inf_le_left _ _ _ := mem_inf_of_left
  inf_le_right _ _ _ := mem_inf_of_right
  le_inf := fun _ _ _ h₁ h₂ _s ⟨_a, ha, _b, hb, hs⟩ => hs.symm ▸ inter_mem (h₁ ha) (h₂ hb)
  le_sSup _ _ h₁ _ h₂ := h₂ h₁
  sSup_le _ _ h₁ _ h₂ _ h₃ := h₁ _ h₃ h₂
  sInf_le _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds]; exact fun _ h₃ ↦ h₃ h₁ h₂
  le_sInf _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds] at h₂; exact h₂ h₁
  le_top _ _ := univ_mem'
  bot_le _ _ _ := trivial

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