English
The preimage of Ioc(a,b] under the integer embedding is Ioc(⌊a⌋, ⌊b⌋).
Русский
Обратное образующее множество Ioc(a,b] под встроенным отображением целых чисел даёт Ioc(⌊a⌋, ⌊b⌋).
LaTeX
$$$((\\uparrow): \\mathbb{Z} \\to \\mathbb{R})^{-1}(\\mathrm{Ioc}(a,b]) = \\mathrm{Ioc}(\\lfloor a \\rfloor, \\lfloor b \\rfloor)$$$
Lean4
@[simp]
theorem preimage_Ioc {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋ :=
by
ext
simp [floor_lt, le_floor]