preimage_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_Ico {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉ :=
  by
  ext
  simp [ceil_le, lt_ceil]

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