isInducing_pullback_to_prod — Mathlib

English

The map from the pullback to the product given by the two projections is inducing, i.e., the pullback topology is the subspace topology induced from the product.

Русский

Отображение предела в произведение, заданное двумя проекциями, индукцирующее; топология предела совпадает с подпространственной топологией произведения.

LaTeX

$$$ \operatorname{IsInducing}\left|\iota\right| = \text{the map } \mathrm{prod.lift}( \mathrm{pullback.fst} f g, \mathrm{pullback.snd} f g) \right)$$

Lean4

theorem isInducing_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsInducing <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) :=
  ⟨by simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]⟩

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