symm — Mathlib

English

The AntivaryOn relation is symmetric: swapping the roles of f and g preserves AntivaryOn on a set.

Русский

Антивариантность на множестве симметрична: при смене ролей f и g сохраняется AntivaryOn.

LaTeX

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

Lean4

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

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