eq_replicate — Mathlib

English

An element s ∈ Sym α n equals replicate n a iff every element of s equals a.

Русский

Элемент s ∈ Sym α n равен replicate n a тогда и только тогда, когда каждый элемент s равен a.

LaTeX

$$$ s = \mathrm{replicate}(n,a) \iff \forall b \in s, b = a. $$$

Lean4

theorem eq_replicate {a : α} {n : ℕ} {s : Sym α n} : s = replicate n a ↔ ∀ b ∈ s, b = a :=
  Subtype.ext_iff.trans <| Multiset.eq_replicate.trans <| and_iff_right s.prop

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