le_floor

Mathlib.Algebra.Order.Floor.Defs

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

English

If a ∈ α and n ∈ ℕ, and a ≥ n, then n ≤ ⌊a⌋₊.

Русский

Если a ∈ α и n ∈ ℕ, и a ≥ n, тогда n ≤ ⌊a⌋₊.

LaTeX

$$$\forall a \in \alpha, \forall n \in \mathbb{N}, a \ge n \Rightarrow n \le \lfloor a \rfloor_{+}$$$

Lean4

theorem le_floor [IsOrderedRing α] (h : (n : α) ≤ a) : n ≤ ⌊a⌋₊ :=
  (le_floor_iff <| n.cast_nonneg.trans h).2 h

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

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

Разделы

Аффилиация

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