encard_univ_coe

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_univ_coe

English

For any set s, encard(univ : Set s) = encard s.

Русский

encard(univ : Set s) = encard s для множества s.

LaTeX

$$$ \operatorname{encard}(\mathrm{univ} : Set\, s) = \operatorname{encard}(s) $$$

Lean4

@[deprecated "Use simp" (since := "2025-09-23")]
theorem encard_univ_coe (s : Set α) : encard (univ : Set s) = encard s := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru