monovaryOn_comm — Mathlib

English

Let α, β be linearly ordered sets and f : ι → α, g : ι → β. For any s ⊆ ι, the relation MonovaryOn f g s is equivalent to MonovaryOn g f s.

Русский

Пусть α, β — линейно упорядоченные множества, f: ι → α, g: ι → β. Для любого подмножества s ⊆ ι выполняется эквивалентность MonovaryOn f g s и MonovaryOn g f s.

LaTeX

$$$\\forall {\\iota}, {\\alpha}, {\\beta}, \\text{ если } \\text{LinearOrder}(\\alpha), \\text{LinearOrder}(\\beta), \\ f: \\iota \\to \\alpha, \\ g: \\iota \\to \\beta, \\ MonovaryOn f g s \\iff MonovaryOn g f s$$$

Lean4

theorem monovaryOn_comm : MonovaryOn f g s ↔ MonovaryOn g f s :=
  ⟨MonovaryOn.symm, MonovaryOn.symm⟩

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