is_basis — Mathlib

English

A Realizer for a Ctop induces a topological basis from the range of its open-set map.

Русский

Реализатор Ctop порождает топологический базис из образа отображения открытых множеств.

LaTeX

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

Lean4

protected theorem is_basis [T : TopologicalSpace α] (F : Realizer α) :
    TopologicalSpace.IsTopologicalBasis (Set.range F.F.f) := by have := toTopsp_isTopologicalBasis F.F;
  rwa [F.eq] at this

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