Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
  P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)

Alias of CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

3 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsLocalAtSource