le_iff_le

Mathlib.Analysis.AbsoluteValue.Equivalence

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.IsEquiv.le_iff_le

English

If v is equivalent to w, then for all x, y we have v x ≤ v y iff w x ≤ w y.

Русский

Если v эквивалентно w, то для любых x,y верно: v x ≤ v y эквивалентно w x ≤ w y.

LaTeX

$$$\\forall x,y: v x \\le v y \\iff w x \\le w y$ under $v.IsEquiv w$$$

Lean4

theorem le_iff_le (h : v.IsEquiv w) {x y : R} : v x ≤ v y ↔ w x ≤ w y :=
  h ..

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

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

Разделы

Аффилиация

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