preimage_Iic

Mathlib.Algebra.Order.Floor.Semiring

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

English

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

Русский

Для любого a, предобраз IIC равен Iic(⌊a⌋₊).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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