pos_of_floor_pos

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.pos_of_floor_pos

English

If 0 < ⌊a⌋₊, then 0 < a.

Русский

Если 0 < ⌊a⌋₊, то 0 < a.

LaTeX

$$$$\text{If } 0 < \lfloor a \rfloor_{+},\ \ 0 < a.$$$$

Lean4

theorem pos_of_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
  (le_or_gt a 0).resolve_left fun ha => lt_irrefl 0 <| by rwa [floor_of_nonpos ha] at h

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

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

Разделы

Аффилиация

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