Topology of affine subspaces.

This file defines the embedding map from an affine subspace to the ambient space as a continuous affine map.

Main definitions

• AffineSubspace.subtypeA is AffineSubspace.subtype as a ContinuousAffineMap.

def AffineSubspace.subtypeA {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ↥s →ᴬ[R] P

Embedding of an affine subspace to the ambient space, as a continuous affine map.

Equations

• s.subtypeA = { toAffineMap := s.subtype, cont := ⋯ }

@[simp]

theorem AffineSubspace.coe_subtypeA {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ⇑s.subtypeA = Subtype.val

@[simp]

theorem AffineSubspace.subtypeA_toAffineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ↑s.subtypeA = s.subtype

instance AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [TopologicalSpace V] [IsTopologicalAddTorsor P] {s : AffineSubspace R P} [Nonempty ↥s] : IsTopologicalAddTorsor ↥s

theorem AffineSubspace.isClosed_direction_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [TopologicalSpace V] [IsTopologicalAddTorsor P] [T1Space V] (s : AffineSubspace R P) : IsClosed ↑s.direction ↔ IsClosed ↑s