projective_of_extrDisc — Mathlib

English

If X is ExtremallyDisconnected in Profinite, then X is projective.

Русский

Если X экстремально разобщено в Profinite, то X проективно.

LaTeX

$$$\text{projective}(X) \text{ if } \operatorname{ExtremallyDisconnected}(X)$$$

Lean4

theorem projective_of_extrDisc {X : Profinite.{u}} (hX : ExtremallyDisconnected X) : Projective X :=
  by
  change Projective (Stonean.toProfinite.obj ⟨X.toTop, inferInstance⟩)
  exact inferInstance

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