hasBasis_biInf_principal — Mathlib

English

If S is directed on a subset of indices and nonempty, then the infimum over i ∈ S of 𝓟(s i) has basis given by i ∈ S with s i.

Русский

Если S направлено по части индексов и непусто, то инфимума по i ∈ S от 𝓟(s(i)) имеет базис, заданный i ∈ S и s(i).

LaTeX

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

Lean4

theorem hasBasis_biInf_principal {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o (· ≥ ·)) S) (ne : S.Nonempty) :
    (⨅ i ∈ S, 𝓟 (s i)).HasBasis (fun i => i ∈ S) s :=
  ⟨fun t => by
    refine mem_biInf_of_directed ?_ ne
    rw [directedOn_iff_directed, ← directed_comp] at h ⊢
    refine h.mono_comp _ ?_
    exact fun _ _ => principal_mono.2⟩

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