zero_mem_box

Mathlib.Order.Interval.Finset.Box

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

English

The zero element belongs to box n if and only if n = 0.

Русский

Ноль принадлежит box(n) тогда и только тогда, когда n = 0.

LaTeX

$$$(0) \in \mathrm{box}(n) \iff n = 0$$$

Lean4

@[simp]
theorem zero_mem_box : (0 : α) ∈ box n ↔ n = 0 := by cases n <;> simp [box_succ_eq_sdiff]

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

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

Разделы

Аффилиация

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