mem_nsmul — Mathlib

English

For multisets, a ∈ n • s iff n ≠ 0 and a ∈ s.

Русский

Для мультимножеств: a ∈ n • s эквивалентно n ≠ 0 и a ∈ s.

LaTeX

$$$ a \in n \cdot s \iff n \neq 0 \land a \in s $$$

Lean4

@[simp]
theorem mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s :=
  by
  refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
  · rintro rfl
    simp [zero_nsmul] at ha
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1
  rw [succ_nsmul, mem_add]
  exact Or.inr h.2

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