range_injOn_strictAnti — Mathlib

English

Similarly, for StrictAnti functions under a well-founded GT order, the range is injective.

Русский

Аналогично для StrictAnti при хорошо упорядоченном GT, диапазон инъективен.

LaTeX

$$$\\text{Set.InjOn }\\text{Set.range }\\{f:\\beta\\to\\gamma \\mid \\text{StrictAnti } f\\}$$$

Lean4

theorem range_injOn_strictAnti [WellFoundedGT β] : Set.InjOn Set.range {f : β → γ | StrictAnti f} := fun _ hf _ hg ↦
  Set.range_injOn_strictMono (β := βᵒᵈ) hf.dual hg.dual

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