inducing_pullbackTotalSpaceEmbedding

English

The embedding that sends a parameter to the pullback total space is an inducing map.

Русский

Встраивание параметра в общее пространство pullback образует индуцирующее отображение.

LaTeX

$$$\mathrm{IsInducing}(\mathrm{pullbackTotalSpaceEmbedding}\ f)$$$

Lean4

theorem inducing_pullbackTotalSpaceEmbedding (f : B' → B) : IsInducing (@pullbackTotalSpaceEmbedding B F E B' f) :=
  by
  constructor
  simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose, Pullback.TotalSpace.topologicalSpace,
    pullbackTopology_def]
  rfl

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