isBasis_basic_opens — Mathlib

English

In terms of subsums, the basic opens indeed constitute a basis for the opens.

Русский

Базис базисных открытых множеств действительно образует базис для открытых множеств.

LaTeX

$$$$ \\text{IsTopologicalBasis}( \\mathrm{range}(\\mathrm{basicOpen}) ). $$$$

Lean4

theorem isBasis_basic_opens : TopologicalSpace.Opens.IsBasis (Set.range (@basicOpen R _)) :=
  by
  unfold TopologicalSpace.Opens.IsBasis
  convert isTopologicalBasis_basic_opens (R := R)
  rw [← Set.range_comp]
  rfl

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