English
Left multiplication by a unit a gives an order isomorphism of ENNReal; equivalently, multiplying on the left by a fixed nonzero finite a preserves the order structure.
Русский
Умножение слева на единицу a, где a обратимо и конечна, задаёт изоморфизм по порядку на ENNReal; умножение слева сохраняет порядок.
LaTeX
$$$\\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; IsUnit(a) \\Rightarrow \\mathbb{R}_{\\ge 0}^{\\infty} \\simeq_{\\mathrm{ord}} \\mathbb{R}_{\\ge 0}^{\\infty}$ по отображению умножения на a слева$$
Lean4
/-- Right multiplication by a nonzero finite `a` as an order isomorphism. -/
@[simps! toEquiv apply symm_apply]
def mulRightOrderIso (a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ ≃o ℝ≥0∞
where
toEquiv := ha.unit.mulRight
map_rel_iff' := by simp [ENNReal.mul_le_mul_right, ha.ne_zero, (isUnit_iff.1 ha).2]
