cutMap_mono

Mathlib.Algebra.Order.CompleteField

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

English

If a1 ≤ a2, then cutMap β a1 ⊆ cutMap β a2.

Русский

Если a1 ≤ a2, то cutMap β a1 ⊆ cutMap β a2.

LaTeX

$$$\text{cutMap}_{β}(a_1) \subseteq \text{cutMap}_{β}(a_2)\quad \text{если } a_1 \le a_2$$$

Lean4

theorem cutMap_mono (h : a₁ ≤ a₂) : cutMap β a₁ ⊆ cutMap β a₂ :=
  image_mono fun _ => h.trans_lt'

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

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

Разделы

Аффилиация

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