to_isTopologicalAddGroup — Mathlib

English

The underlying group of a topological additive torsor is a topological group.

Русский

Вещественная группа тора‑массивной структуры имеет топологическую группу.

LaTeX

$$$ IsTopologicalAddGroup V $$$

Lean4

/-- The underlying group of a topological torsor is a topological group. This is not an instance, as
`P` cannot be inferred. -/
theorem to_isTopologicalAddGroup : IsTopologicalAddGroup V
    where
  continuous_add := by
    have ⟨p⟩ : Nonempty P := inferInstance
    conv =>
      enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]
    fun_prop
  continuous_neg := by
    have ⟨p⟩ : Nonempty P := inferInstance
    conv =>
      enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
    fun_prop

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