hasPullbacksOfInclusions — Mathlib

English

Theorem stating that under hypotheses, HasExplicitPullbacksOfInclusions P holds.

Русский

Теорема, утверждающая, что при данных гипотезах выполняется HasExplicitPullbacksOfInclusions P.

LaTeX

$$$\\text{HasExplicitPullbacksOfInclusions } P$$$

Lean4

theorem hasPullbacksOfInclusions
    (hP' : ∀ ⦃X Y B : CompHausLike.{u} P⦄ (f : X ⟶ B) (g : Y ⟶ B) (_ : IsOpenEmbedding f), HasExplicitPullback f g) :
    HasExplicitPullbacksOfInclusions P :=
  {
    hasProp := by
      intro _ _ _ f
      apply hP'
      exact Sigma.isOpenEmbedding_ι _ _ }

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