instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection

English

The subtype of an affine subspace carries a natural topological affine torsor structure; in particular, it inherits a topological AddTorsor structure.

Русский

Подмножество аффинного подпространства наследует естественную топологическую аффиннуюtorsor-структуру; в частности, обладает топологической структурой AddTorsor.

LaTeX

$$IsTopologicalAddTorsor(Subtype x ∈ s) $$

Lean4

instance {s : AffineSubspace R P} [Nonempty s] : IsTopologicalAddTorsor s
    where
  continuous_vadd := by
    rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
    fun_prop
  continuous_vsub := by
    rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
    fun_prop

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