inj

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.inj

English

For a normal f, f is injective: f(a) = f(b) iff a = b.

Русский

Для нормальной функции f выполнено: f(a) = f(b) тогда и только тогда, когда a = b.

LaTeX

$$$\forall f\,\bigl(\mathrm{IsNormal}(f)\bigr)\; \forall a b,\; f(a) = f(b) \iff a = b.$$$

Lean4

theorem inj {f} (H : IsNormal f) {a b} : f a = f b ↔ a = b := by simp only [le_antisymm_iff, H.le_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru