forall_in_swap — Mathlib

English

Interchanging the order of universal quantifiers between a filter membership and an auxiliary variable does not change the statement.

Русский

Поменяние порядка квантификации между принадлежностью фильтру и дополнительной переменной не меняет смысл утверждения.

LaTeX

$$$ (\forall a \in f, \forall b,\ p(a,b)) \iff (\forall b,\forall a \in f,\ p(a,b)). $$$

Lean4

@[deprecated forall_swap (since := "2025-06-10")]
theorem forall_in_swap {β : Type*} {p : Set α → β → Prop} : (∀ a ∈ f, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ f, p a b := by tauto

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