count_attach — Mathlib

English

For any s and a = ⟨x, hx⟩ with x ∈ s, the number of occurrences of a in s.attach equals the number of occurrences of x in s.

Русский

Для любого s и элемента a = ⟨x, hx⟩ типа {x ∈ s} число вхождений a в s.attach равно числу вхождений x в s.

LaTeX

$$$\operatorname{count}(a, s.\mathrm{attach}) = \operatorname{count}(a.\mathrm{val}, s)$$$

Lean4

@[simp]
theorem count_attach (a : { x // x ∈ s }) : s.attach.count a = s.count ↑a :=
  Eq.trans (countP_congr rfl fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _

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