eq_iInf_principal — Mathlib

English

The filter generated by a FilterBasis B equals the infimum of the principal filters on all sets in B.

Русский

Фильтр, порождённый базисом фильтров B, равен инфимуму главных фильтров на все множества, принадлежащие B.

LaTeX

$$$B.filter = \bigwedge_{s \in B.sets} \mathcal{P}(s)$$$

Lean4

theorem eq_iInf_principal (B : FilterBasis α) : B.filter = ⨅ s : B.sets, 𝓟 s :=
  by
  have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) :=
    by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub
  ext U
  simp [mem_filter_iff, mem_iInf_of_directed this]

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