range_inj — Mathlib

English

If f and g are StrictAnti, 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$ (для StrictAnti f,g)$$

Lean4

theorem range_inj [WellFoundedGT β] {f g : β → γ} (hf : StrictAnti f) (hg : StrictAnti g) :
    Set.range f = Set.range g ↔ f = g :=
  Set.range_injOn_strictAnti.eq_iff hf hg

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