range_inj — Mathlib

English

Two order embeddings on a well-ordered type are equal iff they have the same range.

Русский

Два вложения порядка на хорошо упорядоченном множество равны тогда и только тогда, когда их диапазоны совпадают.

LaTeX

$$$\mathrm{range}(f) = \mathrm{range}(g) \iff f = g$$$

Lean4

/-- Two order embeddings on a well-order are equal provided that their ranges are equal. -/
theorem range_inj [LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} : Set.range f = Set.range g ↔ f = g :=
  by rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]

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