homOfLE_isIso_of_eq — Mathlib

English

If x ≤ y and x = y, then homOfLE(h) is an isomorphism (its inverse is homOfLE(le_of_eq heq.symm)).

Русский

Если x ≤ y и x = y, то homOfLE(h) является изоморфизмом (обратный задаётся как homOfLE(le_of_eq heq.symm)).

LaTeX

$$$\mathrm{homOfLE\_isIso\_of\_eq} : (h : x \le y) \to (heq : x = y) \Rightarrow \mathrm{IsIso}(\mathrm{homOfLE}(h)).$$$

Lean4

theorem homOfLE_isIso_of_eq {x y : X} (h : x ≤ y) (heq : x = y) : IsIso (homOfLE h) :=
  ⟨homOfLE (le_of_eq heq.symm), by simp⟩

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