preimage_floor_zero

Mathlib.Algebra.Order.Floor.Semiring

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

English

The preimage of {0} under floor is Iio 1, i.e., { x : R | floor(x) = 0 } = { x | x < 1 }.

Русский

Образ данного нулевого значения под floor равен Iio 1: {x | floor(x) = 0} = {x | x < 1}.

LaTeX

$$(floor : R → ℕ)^{-1}'{0} = \mathrm{Iio}(1)$$

Lean4

@[simp]
theorem preimage_floor_zero : (floor : R → ℕ) ⁻¹' {0} = Iio 1 :=
  ext fun _ => floor_eq_zero

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

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

Разделы

Аффилиация

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