of_monotoneOn_strictAntiOn — Mathlib

English

If f is monotone on s and strictly anti 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_monotoneOn_strictAntiOn (hf : MonotoneOn f s) (hf' : StrictAntiOn f s) : IsAntichain (· ≤ ·) s :=
  fun _a ha _b hb hab' hab ↦ (hf ha hb hab).not_gt (hf' ha hb <| hab.lt_of_ne hab')

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