preimage_Ioo — Mathlib

English

If a ≥ 0, then { n ∈ ℕ | a < n < b } equals { n ∈ ℕ | ⌊a⌋₊ < n < ⌈b⌉₊ }.

Русский

Если a ≥ 0, то { n ∈ ℕ | a < n < b } равно { n ∈ ℕ | ⌊a⌋₊ < n < ⌈b⌉₊ }.

LaTeX

$$$a \ge 0 \Rightarrow \{n \in \mathbb{N} : a < n < b\} = \{n \in \mathbb{N} : \lfloor a \rfloor_{+} < n < \lceil b \rceil_{+} \}$$$

Lean4

@[simp]
theorem preimage_Ioo {a b : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊ :=
  by
  ext
  simp [floor_lt, lt_ceil, ha]

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