preimage_Ioc — Mathlib

English

The preimage of the half-open interval Ioc a b under Nat.cast is the interval ⌊a⌋₊ ≤ n ≤ ⌊b⌋₊.

Русский

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

LaTeX

$$$\{n \in \mathbb{N} : a < n \le b\} = \{n \in \mathbb{N} : \lfloor a \rfloor_{+} \le n \le \lfloor b \rfloor_{+} \}$$$

Lean4

@[simp]
theorem preimage_Ioc {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊ :=
  by
  ext
  simp [floor_lt, le_floor_iff, hb, ha]

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