ncard_coe — Mathlib

English

For any subset s of α, the ncard of the set of elements of s (the subtype) equals the ncard of s.

Русский

Для любого подмножества s множества α кардинальность множества элементов этого подмножества равна кардинальности самого подмножества.

LaTeX

$$$$ \mathrm{Set}.\mathrm{ncard}(\mathrm{univ} : \mathrm{Set}(\mathrm{Set.Elem}(s))) = s.ncard $$$$

Lean4

theorem ncard_coe {α : Type*} (s : Set α) : Set.ncard (Set.univ : Set (Set.Elem s)) = s.ncard := by simp

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