English
If hx ≠ 0 and h'x ≠ ∞ and hy > 1 and h'y ≠ ⊤, then there exists n ∈ ℤ such that x ∈ Ioc (y^n) (y^(n+1)).
Русский
Если hx ≠ 0 и h'x ≠ ∞ и hy > 1 и h'y ≠ ∞, тогда существует n ∈ ℤ, такое что x ∈ Ioc(y^n, y^(n+1)).
LaTeX
$$$\\forall x,y \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; hx:\\; x \\neq 0,\\; h'x:\\; x \\neq \\infty,\\; 1 < y,\\; h'y:\\; y \\neq \\top \\Rightarrow \\exists n \\in \\mathbb{Z}, x \\in Ioc (y^n) (y^{n+1})$$$
Lean4
/-- Left multiplication by a nonzero finite `a` as an order isomorphism. -/
@[simps! toEquiv apply symm_apply]
def mulLeftOrderIso (a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ ≃o ℝ≥0∞
where
toEquiv := ha.unit.mulLeft
map_rel_iff' := by simp [ENNReal.mul_le_mul_left, ha.ne_zero, (isUnit_iff.1 ha).2]
