floor_eq_on_Ico'

Mathlib.Algebra.Order.Floor.Semiring

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

English

For any a in Ico(n, n+1), ⌊a⌋₊ = n.

Русский

Для любого a из Ico(n, n+1) выполняется ⌊a⌋₊ = 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⌋₊ : R) = n := fun x hx =>
  mod_cast floor_eq_on_Ico n x hx

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

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

Разделы

Аффилиация

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