mk_set_ne_zero_iff

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_set_ne_zero_iff

English

A set s is nonempty if and only if its cardinality is nonzero.

Русский

Множество s непусто тогда, когда его кардинальность не равна нулю.

LaTeX

$$$|s| \\neq 0 \\iff s.Nonempty$$$

Lean4

theorem mk_set_ne_zero_iff {α : Type u} (s : Set α) : #s ≠ 0 ↔ s.Nonempty := by rw [mk_ne_zero_iff, nonempty_coe_sort]

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

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

Разделы

Аффилиация

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