preimage_Ioi

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.preimage_Ioi

English

For any a, (Nat.cast)⁻¹' Ioi(a) equals Ioi(⌊a⌋₊).

Русский

Для любого a множество натуральных x, удовлетворяющих x > a, равно Ioi(⌊a⌋₊).

LaTeX

$$$ (\mathrm{Nat.cast})^{-1}(\mathrm{Ioi}(a)) = \mathrm{Ioi}(\lfloor a \rfloor_{+}) $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru