subset_singleton_iff — Mathlib

English

For any a and L, L ⊆ [a] if and only if there exists n with L = replicate(n, a).

Русский

Для любого a и L верно: L ⊆ [a] тогда и только тогда, когда существует n such that L = replicate(n, a).

LaTeX

$$$$\\forall a:\\\\alpha,\\\\forall L:\\\\mathrm{List}\\\\alpha,\\ L \\subseteq [a] \\\\iff \\exists n,\\ L = \\mathrm{replicate}(n, a).$$$$

Lean4

theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = replicate n a := by
  simp only [eq_replicate_iff, subset_def, mem_singleton, exists_eq_left']

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