symm — Mathlib

English

The MonovaryOn relation is symmetric with respect to the pair of functions on a set: swapping the order preserves MonovaryOn.

Русский

Чтобы поменять пары функций на множестве, сохраняется MonovaryOn.

LaTeX

$$$$ \\text{MonovaryOn}(f,g,s) \\iff \\text{MonovaryOn}(g,f,s) $$$$

Lean4

@[symm]
protected theorem symm (h : MonovaryOn f g s) : MonovaryOn g f s := fun _ hi _ hj hf =>
  le_of_not_gt fun hg => hf.not_ge <| h hj hi hg

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