preimage_Ico — Mathlib

English

The preimage of the half-open interval Ico a b under Nat.cast is the half-open interval Ico ⌈a⌉₊ ⌈b⌉₊.

Русский

Предобраз частично открытого интервала Ico a b по Nat.cast даёт Ico ⌈a⌉₊ ⌈b⌉₊.

LaTeX

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

Lean4

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

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