hasBasis_iInf_principal — Mathlib

English

For a directed family s of sets, the infimum of principal filters (over i in S) has a basis with index set S given by membership in S.

Русский

Для направленного семейства s состояний множество индексов S образует базис инфимума по s.

LaTeX

$$$ (\iInf i \in S, 𝓟(s(i))).HasBasis (fun i => i \in S) s $$$

Lean4

theorem hasBasis_iInf_principal {s : ι → Set α} (h : Directed (· ≥ ·) s) [Nonempty ι] :
    (⨅ i, 𝓟 (s i)).HasBasis (fun _ => True) s :=
  ⟨fun t => by simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t⟩

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