floor_eq_on_Ico

Mathlib.Algebra.Order.Floor.Semiring

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

← MathLib Explorer

English

On the interval Ico(n, n+1), the floor is constantly equal to n.

Русский

На интервале Ico(n, n+1) этаж равен постоянно n.

LaTeX

$$∀ a ∈ Set.Ico n.cast (n.cast + 1), \lfloor a \rfloor_+ = n$$

Lean4

theorem floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set R), ⌊a⌋₊ = n := fun _ ⟨h₀, h₁⟩ =>
  (floor_eq_iff <| n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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