divLeft — Mathlib

English

For any element x ∈ G, the map y ↦ x / y is a homeomorphism of G with the group structure.

Русский

Для любого элемента x ∈ G отображение y ↦ x / y является гомеоморфизмом пространства G в той же группе.

LaTeX

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

Lean4

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

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