preimage_Icc — Mathlib

English

The preimage of the closed interval Icc a b under Nat.cast is the interval ⌈a⌉₊ ≤ n ≤ ⌊b⌋₊.

Русский

Предобраз Icc a b по Nat.cast равен ⌈a⌉₊ ≤ n ≤ ⌊b⌋₊.

LaTeX

$$$\{n \in \mathbb{N} : a \le n \le b\} = \{n \in \mathbb{N} : \lceil a \rceil_{+} \le n \le \lfloor b \rceil_{+} \}$$$

Lean4

@[simp]
theorem preimage_Icc {a b : R} (hb : 0 ≤ b) : (Nat.cast : ℕ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊ :=
  by
  ext
  simp [ceil_le, hb, le_floor_iff]

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