finitaryExtensive — Mathlib

English

If a property P on CompHausLike behaves well with explicit finite coproducts and pullbacks along open embeddings, then CompHausLike P is finitary extensive.

Русский

Если свойство P над CompHausLike хорошо себя ведет по отношению к явным конечным coproducts и pullbacks по открытым вложениям, то CompHausLike P является конечносвязным экстенсивным.

LaTeX

$$$\\mathrm{FinitaryExtensive}(\\mathrm{CompHausLike}(P))$$$

Lean4

theorem finitaryExtensive
    (hP' : ∀ ⦃X Y B : CompHausLike.{u} P⦄ (f : X ⟶ B) (g : Y ⟶ B) (_ : IsOpenEmbedding f), HasExplicitPullback f g) :
    FinitaryExtensive (CompHausLike P) :=
  have := hasPullbacksOfInclusions hP'
  finitaryExtensive_of_preserves_and_reflects (compHausLikeToTop P)

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