grade_injective — Mathlib

English

The grade map is injective when α is linearly ordered: grade(a) = grade(b) implies a = b.

Русский

Градационная функция инъективна при линейном порядке: grade(a) = grade(b) ⇒ a = b.

LaTeX

$$$\text{grade}\colon \alpha \to 𝕆\;\text{ is injective: }\; \mathrm{grade}(a)=\mathrm{grade}(b) \Rightarrow a=b.$$$

Lean4

theorem grade_injective : Function.Injective (grade 𝕆 : α → 𝕆) :=
  grade_strictMono.injective

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