encard_lt_top_iff

Mathlib.Data.Set.Card

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

English

For any s, encard s < ⊤ iff s is finite.

Русский

Для любого s: encard s < ⊤ тогда и только тогда, когда s конечно.

LaTeX

$$$ s.encard < \top \iff s.Finite $$$

Lean4

@[simp]
theorem encard_lt_top_iff : s.encard < ⊤ ↔ s.Finite :=
  ⟨fun h ↦ by_contra fun h' ↦ h.ne (Infinite.encard_eq h'), Finite.encard_lt_top⟩

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

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

Разделы

Аффилиация

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