preimage_Iio

Mathlib.Algebra.Order.Floor.Semiring

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

English

For any a, (Nat.cast)⁻¹' Iio(a) equals Iio(⌈a⌉₊).

Русский

Для любого a, предобраз IIO равен Iio(⌈a⌉₊).

LaTeX

$$$ (\mathrm{Nat.cast})^{-1}(\mathrm{Iio}(a)) = \mathrm{Iio}(\lceil a \rceil_{+}) $$$

Lean4

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

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

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

Разделы

Аффилиация

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