one_le_iff_pos

Mathlib.SetTheory.Cardinal.Basic

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

English

1 ≤ c if and only if 0 < c.

Русский

1 ≤ c тогда и только если 0 < c.

LaTeX

$$$1 \le c \iff 0 < c$$$

Lean4

theorem one_le_iff_pos {c : Cardinal} : 1 ≤ c ↔ 0 < c := by rw [← succ_zero, succ_le_iff]

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

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

Разделы

Аффилиация

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