lt_one_iff — Mathlib

English

If v is equivalent to w, then for all x, v x < 1 iff w x < 1 (under domain assumptions).

Русский

Если v эквивалентно w, то для любого x верно: v x < 1 тогда и только тогда, когда w x < 1 (при определённых условиях на область).

LaTeX

$$$\\forall x,\\; v.IsEquiv w \\Rightarrow (v x < 1) \\Leftrightarrow (w x < 1)$$$

Lean4

theorem lt_one_iff (h : v.IsEquiv w) {x : R} : v x < 1 ↔ w x < 1 := by simpa only [map_one] using h.lt_iff_lt (y := 1)

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