forall — Mathlib

English

For every property p on Sym α n, p holds for all elements iff p holds for all mk representations.

Русский

Для любого свойства p на Sym α n верно: p для всех элементов ↔ p для всех представлений mk.

LaTeX

$$$ (\forall s:\mathrm{Sym}(\alpha,n), p(s)) \iff (\forall (s:\mathrm{Multiset}(\alpha)) (hs:\mathrm{card}(s)=n), p(\mathrm{mk}(s,hs))) $$$

Lean4

theorem «forall» {p : Sym α n → Prop} :
    (∀ s : Sym α n, p s) ↔ ∀ (s : Multiset α) (hs : Multiset.card s = n), p (Sym.mk s hs) := by simp [Sym]

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