isIso_restrictionToTruncGE' — Mathlib

English

If i is not a boundary, then the restriction map f i is an isomorphism.

Русский

Если i не является границей, то ограничивающее отображение f i является изоморфизмом.

LaTeX

$$$IsIso\bigl((K.restrictionToTruncGE' e).f i\bigr)$$$

Lean4

/-- `K.restrictionToTruncGE' e).f i` is an isomorphism when `¬ e.BoundaryGE i`. -/
theorem isIso_restrictionToTruncGE' (i : ι) (hi : ¬e.BoundaryGE i) : IsIso ((K.restrictionToTruncGE' e).f i) :=
  by
  rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]
  infer_instance

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