isIso_truncLE'ToRestriction — Mathlib

English

If i is not in BoundaryLE, then the component (K.truncLE'ToRestriction e).f i is an isomorphism.

Русский

Если i не лежит в BoundaryLE, то компонент (K.truncLE'ToRestriction e).f i является изоморфизмом.

LaTeX

$$$\text{IsIso}\bigl((K.truncLE'ToRestriction e).f i\bigr)$$$

Lean4

/-- `(K.truncLE'ToRestriction e).f i` is an isomorphism when `¬ e.BoundaryLE i`. -/
theorem isIso_truncLE'ToRestriction (i : ι) (hi : ¬e.BoundaryLE i) : IsIso ((K.truncLE'ToRestriction e).f i) :=
  by
  change IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop
  have := K.op.isIso_restrictionToTruncGE' e.op i (by simpa)
  infer_instance

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