mk_of_iff — Mathlib

English

If P is stable under base change, then the universally extended P is stable under base change.

Русский

Если P устойчиво к изменению основания, то универсальное расширение P устойчиво к базовому изменению.

LaTeX

$$$P^{\mathrm{universally}}.IsStableUnderBaseChange$$$

Lean4

theorem mk_of_iff [P.RespectsIso]
    (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : Precoverage.ZeroHypercover.{v} K Y), P f ↔ ∀ i, P (pullback.snd f (𝒰.f i))) :
    P.IsLocalAtTarget K where
  pullbackSnd 𝒰 i h := (H _ 𝒰).mp h i
  of_zeroHypercover 𝒰 h := (H _ 𝒰).mpr h

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