natCard_pos

Mathlib.SetTheory.Cardinal.Finite

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

← MathLib Explorer

English

For a finite set s, 0 < Nat.card s if and only if s is nonempty.

Русский

Для конечного множества s выполняется: 0 < Nat.card s тогда и только тогда, когда s непусто.

LaTeX

$$$$ 0 < Nat.card(s) \iff s.Nonempty $$$$

Lean4

theorem natCard_pos (hs : s.Finite) : 0 < Nat.card s ↔ s.Nonempty := by
  simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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