floor_eq_on_Ico

Mathlib.Algebra.Order.Floor.Ring

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

English

For any integer n, and any a ∈ Ico (n, n+1), ⌊a⌋ = n.

Русский

Для любого целого n и любого a ∈ Ico(n, n+1) имеем ⌊a⌋ = n.

LaTeX

$$$$ a \\in \\mathrm{Ico}(n, n+1) \\Rightarrow \\lfloor a \\rfloor = n $$$$

Lean4

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

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

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

Разделы

Аффилиация

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