one_le_card

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.one_le_card

English

For any Finset s, 1 ≤ #s iff s.Nonempty.

Русский

Для любого Finset s, 1 ≤ #s тогда и только тогда s непуст.

LaTeX

$$$1 \le \#s \iff s.Nonempty$$$

Lean4

@[simp]
theorem one_le_card : 1 ≤ #s ↔ s.Nonempty :=
  card_pos

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

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

Разделы

Аффилиация

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