preimage_Ioc — Mathlib

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]

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