range_inj — Mathlib

English

If f and g are StrictMono, then Set.range f = Set.range g iff f = g.

Русский

Если f и g строго монотонны, то диапазоны равны тогда и только тогда, когда функции равны.

LaTeX

$$$\\text{Range inj} : \\text{Set.range }f = \\text{Set.range }g \\iff f = g$ (для StrictMono f,g)$$

Lean4

theorem range_inj [WellFoundedLT β] {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g) :
    Set.range f = Set.range g ↔ f = g :=
  Set.range_injOn_strictMono.eq_iff hf hg

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