iInf — Mathlib

English

Infimum-induced basis via preimages under maps provides a basis for the induced inf topology.

Русский

Базис инфимного сверху через предобраз множества образует базис для инфимной топологии.

LaTeX

$$$\\text{IsTopologicalBasis}(t := \\operatorname{induced} f_1 t \\sqcap \\operatorname{induced} f_2 s)\\; (\\text{image2}(f_1^{-1}'\\cdot \\cap f_2^{-1}'\\cdot)\\; B_1\\; B_2)$$$

Lean4

protected theorem iInf {β : Type*} {ι : Type*} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)}
    (h_basis : ∀ i, IsTopologicalBasis (t := t i) (T i)) :
    IsTopologicalBasis (t := ⨅ i, t i)
      {S | ∃ (U : ι → Set β) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} :=
  by
  let _ := ⨅ i, t i
  refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
  · rintro - ⟨U, F, hU, rfl⟩
    refine isOpen_biInter_finset fun i hi ↦ (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)
  · intro a u ha hu
    rcases
      (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf' (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1
        (hu.mem_nhds ha) with
      ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
    refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]
    · exact fun i hi ↦ (hU i hi).1
    · exact fun i hi ↦ (hU i hi).2
    · exact hUu

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