exists — Mathlib

English

There exists an s in Sym α n with property p iff there exists a multiset and hs with card n such that p holds for mk(s,h).

Русский

Существует s ∈ Sym α n с свойством p тогда и только тогда, когда существует мультимножество s и число hs с card n, такое что p( mk(s,hs) ).

LaTeX

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

Lean4

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

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