vaddConst — Mathlib

English

For a topological V-torsor P and every p in P, the map v ↦ v +ᵥ p is a homeomorphism from V onto P.

Русский

Для топологического торсора V над P и каждого p в P отображение v ↦ v +ᵥ p является гомеоморфизмом V в P.

LaTeX

$$$\\forall p \\in P,\\ \\exists h: V \\to P \\text{ such that } h \\text{ is a homeomorphism and } h(v)=v +\\!\\,ᵥ p,\\ h^{-1}(x)=x -\\!\\,ᵥ p.$$$

Lean4

/-- The map `v ↦ v +ᵥ p` as a homeomorphism between `V` and `P`. -/
@[simps!]
def vaddConst (p : P) : V ≃ₜ P where
  __ := Equiv.vaddConst p
  continuous_toFun := by fun_prop
  continuous_invFun := by fun_prop

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