induced — Mathlib

English

Under the induced topology, a basis is given by preimages of a basis on the target space.

Русский

При индуцированной топологии базис задаётся как предобраз базиса на целевом пространстве.

LaTeX

$$$IsTopologicalBasis\bigl(t := induced f s\bigr)\bigl((preimage f) '' T\bigr).$$$

Lean4

protected theorem induced {α} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)} (h : IsTopologicalBasis T) :
    IsTopologicalBasis (t := induced f s) ((preimage f) '' T) :=
  h.isInducing (t := induced f s) (.induced f)

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