divRight — Mathlib

English

The map x ↦ x / a is a homeomorphism of G for any a ∈ G.

Русский

Отображение x ↦ x / a является гомеоморфизмом G.

LaTeX

$$$\text{divRight}(a): G \to G \text{ is a homeomorphism.}$$$

Lean4

/-- A version of `Homeomorph.mulRight a⁻¹ b` that is defeq to `b / a`. -/
@[to_additive (attr := simps! +simpRhs) /-- A version of `Homeomorph.addRight (-a) b` that is defeq to `b - a`. -/
    ]
def divRight (x : G) : G ≃ₜ G :=
  { Equiv.divRight x with
    continuous_toFun := continuous_id.div' continuous_const
    continuous_invFun := continuous_id.mul continuous_const }

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