forall_swap — Mathlib

English

The order of universal quantifiers can be swapped: (∀ x y, p x y) is equivalent to (∀ y x, p x y).

Русский

Порядок обобщённых по переменным можно поменять: (∀ x y, p x y) эквивалентно (∀ y x, p x y).

LaTeX

$$$\\\\forall x y, p x y\\\\leftrightarrow\\\\forall y x, p x y$$$

Lean4

theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
  ⟨fun f x y ↦ f y x, fun f x y ↦ f y x⟩

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