eq_replicate_iff — Mathlib

English

Let s be an element of Sym α n and a ∈ α. Then s = replicate n a if and only if every element of s equals a.

Русский

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

LaTeX

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

Lean4

theorem eq_replicate_iff : s = replicate n a ↔ ∀ b ∈ s, b = a :=
  by
  rw [Subtype.ext_iff, val_replicate, Multiset.eq_replicate]
  exact and_iff_right s.2

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