isInducing — Mathlib

English

If f is an inducing map and B is a topological basis on β, then the image of preimages forms a basis on α.

Русский

Если f — индуциирующее отображение, и B — базис на β, то множество f^{-1}(B) образует базис на α.

LaTeX

$$$IsTopologicalBasis((preimage f) '' B).$$$

Lean4

protected theorem isInducing {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)} (hf : IsInducing f)
    (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) :=
  .of_hasBasis_nhds fun a ↦
    by
    convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
    aesop

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