instEpiAppOppositeNatπAsLimitCone

English

For a LightProfinite object S, and for every i in Opposite Nat, the projection S.asLimitCone.π.app i is epi.

Русский

Для объекта S∈LightProfinite для каждого i в Opposite Nat проекция S.asLimitCone.π.app i является эпиморфизмом.

LaTeX

$$$\forall i:\mathrm{Opposite\ Nat},\ \operatorname{Epi}(S.asLimitCone.π.app i).$$$

Lean4

instance (i : ℕᵒᵖ) : Epi (S.asLimitCone.π.app i) :=
  (epi_iff_surjective _).mpr (S.proj_surjective _)

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