cutMap_self

Mathlib.Algebra.Order.CompleteField

URI: https://scilib.ai/kg/mathlib#LinearOrderedField.cutMap_self

English

Equality: cutMap α a equals Iio(a) ∩ range Rat.cast.

Русский

Равенство: cutMap α a равно Iio(a) ∩ range Rat.cast.

LaTeX

$$$\operatorname{cutMap}_{α}(a) = Iio(a) \cap \operatorname{range}(\operatorname{Rat.cast} : \mathbb{Q} \to α)$$$

Lean4

theorem cutMap_self (a : α) : cutMap α a = Iio a ∩ range (Rat.cast : ℚ → α) := by grind [mem_cutMap_iff]

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

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

Разделы

Аффилиация

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