mk_le

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.mk_le

English

For all f,g in CauSeq(ℚ, abs), the map mk preserves order: mk f ≤ mk g iff f ≤ g.

Русский

Для всех f,g ∈ CauSeq(ℚ, abs) отображение mk сохраняет порядок: mk f ≤ mk g эквивалентно f ≤ g.

LaTeX

$$$mk(f) \le mk(g) \iff f \le g$$$

Lean4

@[simp]
theorem mk_le {f g : CauSeq ℚ abs} : mk f ≤ mk g ↔ f ≤ g := by simp only [le_def', mk_lt, mk_eq]; rfl

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

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

Разделы

Аффилиация

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