floor_eq_self_iff_mem

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.floor_eq_self_iff_mem

English

⌊a⌋ = a if and only if a ∈ Set.range ⌊Int.cast⌋, i.e., a is an integer.

Русский

⌊a⌋ = a тогда и только тогда, когда a ∈ множество образа целых чисел в R.

LaTeX

$$$$\lfloor a \rfloor = a \iff a \in \{\, \uparrow z : z \in \mathbb{Z} \}\,.$$$$

Lean4

theorem floor_eq_self_iff_mem (a : R) : ⌊a⌋ = a ↔ a ∈ Set.range Int.cast := by aesop

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

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

Разделы

Аффилиация

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