antivaryOn_comm — Mathlib

English

Let f: ι → α and g: ι → β with α and β linearly ordered, and s ⊆ ι. Then AntivaryOn f g s holds if and only if AntivaryOn g f s.

Русский

Пусть f: ι → α и g: ι → β, где α и β упорядочены линейно, и s ⊆ ι. Тогда AntivaryOn f g s выполняется тогда и только тогда, когда AntivaryOn g f s выполняется.

LaTeX

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

Lean4

theorem antivaryOn_comm : AntivaryOn f g s ↔ AntivaryOn g f s :=
  ⟨AntivaryOn.symm, AntivaryOn.symm⟩

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