forall_in_swap — Mathlib

English

A deprecated lemma that reorders universal quantifiers over a set; expresses equivalence of the order of universality and membership quantifiers.

Русский

Устаревшая лемма, переставляющая квантор всеобщности над множеством; выражает эквивалентность порядка кванторов.

LaTeX

$$$(\forall a \in s, \forall b, p\,a\,b) \leftrightarrow (\forall b, \forall a \in s, p\,a\,b)$$$

Lean4

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

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