floor_eq_on_Ico'

Mathlib.Algebra.Order.Floor.Ring

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

English

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

Русский

Для каждого целого n и a ∈ Ico(n, n+1) выполняется ⌊a⌋ = n (в R).

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⌋ : R) = n := fun a ha =>
  congr_arg _ <| floor_eq_on_Ico n a ha

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

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

Разделы

Аффилиация

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