of_strictMonoOn_antitoneOn — Mathlib

English

If f: α → β is strictly monotone on a set s and antitone on s, then s is an antichain with respect to ≤.

Русский

Если функция f: α → β строго монотонна на множестве s и антитонна на s, то s является антицепочкой относительно ≤.

LaTeX

$$$\\text{MonotoneOn}(f; s) \\\\land \\\\text{StrictAntiOn}(f; s) \Rightarrow \\operatorname{IsAntichain}(\\le, s)$$$

Lean4

theorem of_strictMonoOn_antitoneOn (hf : StrictMonoOn f s) (hf' : AntitoneOn f s) : IsAntichain (· ≤ ·) s :=
  fun _a ha _b hb hab' hab ↦ (hf ha hb <| hab.lt_of_ne hab').not_ge (hf' ha hb hab)

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