isIso_πTruncGE_iff — Mathlib

English

IsIso(K.πTruncGE e) is equivalent to K being strictly supported along e.

Русский

Изоморфизм πTruncGE(K,e) эквивалентно тому, что K строго поддержан вдоль e.

LaTeX

$$$\text{IsIso}\bigl(K.\pi_{\mathrm{TruncGE}}(e)\bigr) \iff K.\mathrm{IsStrictlySupported}(e)$$$

Lean4

theorem isIso_πTruncGE_iff : IsIso (K.πTruncGE e) ↔ K.IsStrictlySupported e :=
  ⟨fun _ ↦ isStrictlySupported_of_iso (asIso (K.πTruncGE e)).symm e, fun _ ↦ inferInstance⟩

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