toTopsp_isTopologicalBasis — Mathlib

English

The image range of the underlying open sets forms a topological basis for the generated topology.

Русский

Образ диапазона открытых множеств образует базис топологии.

LaTeX

$$$\\text{toTopsp\_basis}(F):\\; \\text{IsTopologicalBasis}(\\text{range }F.f)$$$

Lean4

theorem toTopsp_isTopologicalBasis (F : Ctop α σ) : @TopologicalSpace.IsTopologicalBasis _ F.toTopsp (Set.range F.f) :=
  letI := F.toTopsp
  ⟨fun _u ⟨a, e₁⟩ _v ⟨b, e₂⟩ ↦ e₁ ▸ e₂ ▸ fun x h ↦ ⟨_, ⟨_, rfl⟩, F.inter_mem a b x h, F.inter_sub a b x h⟩,
    eq_univ_iff_forall.2 fun x ↦ ⟨_, ⟨_, rfl⟩, F.top_mem x⟩, rfl⟩

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