of_zeroHypercover_source — Mathlib

English

If P is local at the source with respect to K, and 𝒰 is a zero hypercover of X (with Small 𝒰), then whenever P(𝒰.f i ≫ f) holds for every i, we have P f.

Русский

Если P локально по источнику относительно K, и 𝒰 — нулевой гиперобзор X (с условием Small), то при условии, что для каждого i выполняется P(𝒰.f_i ≫ f), имеем P f.

LaTeX

$$$ IsLocalAtSource(P)\\, K \\;\\Rightarrow\\; \\forall (\\mathcal{U}: ZeroHypercover\\, K X)\\; [ZeroHypercover.Small\\, \\mathcal{U}]\\; (\\forall i, P(\\mathcal{U}.f_i \\gg f)) \\Rightarrow P f $$$

Lean4

theorem of_zeroHypercover_source {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtSource K] {X Y : C}
    {f : X ⟶ Y} (𝒰 : Precoverage.ZeroHypercover.{w} K X) [Precoverage.ZeroHypercover.Small.{v} 𝒰]
    (h : ∀ i, P (𝒰.f i ≫ f)) : P f :=
  by
  rw [IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
  simp [h]

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