eventually_swap_iff — Mathlib

English

For any p: α×β → Prop, p holds eventually in f×g iff p holds for swapped variables in g×f with swap.

Русский

Для любого p: α×β → Prop, верно, что p выполняется почти наверняка в f×g тогда и только тогда, когда p выполняется после перестановки в g×f.

LaTeX

$$$\forall p:\, \alpha \times \beta \rightarrow \mathrm{Prop},\ (\forall^\mathrm{f} x \in f,\ \forall^\mathrm{f} y \in g,\ p(x,y)) \iff (\forall^\mathrm{f} y \in g,\ \forall^\mathrm{f} x \in f,\ p(y,x).swap)$$$

Lean4

theorem eventually_swap_iff {p : α × β → Prop} : (∀ᶠ x : α × β in f ×ˢ g, p x) ↔ ∀ᶠ y : β × α in g ×ˢ f, p y.swap := by
  rw [prod_comm]; rfl

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