exists_swap — Mathlib

English

For a predicate p on two variables, there exists x,y with p x y if and only if there exist y,x with p x y; i.e., the order of existential quantifiers can be swapped.

Русский

Для предиката p, зависящего от двух переменных, существует x,y с p x y тогда и только тогда существует y,x с p x y; порядок существования можно поменять.

LaTeX

$$$$\\exists x\\, \\exists y\\, p(x,y) \\quad\\Longleftrightarrow\\quad \\exists y\\, \\exists x\\, p(x,y).$$$$

Lean4

theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
  ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩

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