IsBasis — Mathlib

English

A family B of open sets is a basis if the corresponding family of their carriers forms a topological basis.

Русский

Множество B открытых множеств является базисом тогда и только тогда, когда соответствующая им коллекция подмножеств образует топологическую базису.

LaTeX

$$$\operatorname{IsBasis}(B) \iff \operatorname{IsTopologicalBasis}\left( \{ U\ply U \in B\} \right)$$$

Lean4

/-- A set of `opens α` is a basis if the set of corresponding sets is a topological basis. -/
def IsBasis (B : Set (Opens α)) : Prop :=
  IsTopologicalBasis (((↑) : _ → Set α) '' B)

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