cast_inj — Mathlib

English

For types α and β with h: α = β, the equality cast h x = cast h y is equivalent to x = y.

Русский

Для типов α и β с h: α = β, равенство cast h x = cast h y эквивалентно x = y.

LaTeX

$$$ \forall {\alpha \beta} (h : \alpha = \beta) {x y : \alpha},\; \operatorname{cast} h x = \operatorname{cast} h y \leftrightarrow x = y$$$

Lean4

@[simp]
theorem cast_inj {α β : Type u} (h : α = β) {x y : α} : cast h x = cast h y ↔ x = y :=
  (cast_bijective h).injective.eq_iff

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