veblenWith_inj — Mathlib

English

The equality of veblenWith values implies equality of inputs, i.e., veblenWith f o a = veblenWith f o b implies a = b.

Русский

Равенство значений veblenWith подразумевает равенство аргументов: veblenWith f o a = veblenWith f o b ⇒ a = b.

LaTeX

$$theorem veblenWith_inj : veblenWith f o a = veblenWith f o b → a = b$$

Lean4

@[simp]
theorem veblenWith_inj : veblenWith f o a = veblenWith f o b ↔ a = b :=
  (veblenWith_injective hf o).eq_iff

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