preimage_Icc — Mathlib

English

The preimage of Icc(a,b) under the integer embedding is Icc(⌈a⌉, ⌊b⌋).

Русский

Обратное образующее множество Icc(a,b) под встраиванием целых чисел равно Icc(⌈a⌉, ⌊b⌋).

LaTeX

$$$((\\uparrow): \\mathbb{Z} \\to \\mathbb{R})^{-1}(\\mathrm{Icc}(a,b)) = \\mathrm{Icc}(\\lceil a \\rceil, \\lfloor b \\rfloor)$$$

Lean4

@[simp]
theorem preimage_Icc {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋ :=
  by
  ext
  simp [ceil_le, le_floor]

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