card_eq_zero

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Set.Infinite.card_eq_zero

English

If s is infinite, then Nat.card s = 0.

Русский

Если множество s бесконечно, то Nat.card s = 0.

LaTeX

$$$ [s.Infinite] \rightarrow \mathrm{Nat.card}\,s = 0 $$$

Lean4

theorem _root_.Set.Infinite.card_eq_zero {s : Set α} (hs : s.Infinite) : Nat.card s = 0 :=
  @card_eq_zero_of_infinite _ hs.to_subtype

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

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

Разделы

Аффилиация

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