Theorems · Theorem · Lie groups
AddTorsor.connectedSpace
∀ (G : Type u_1) (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : TopologicalSpace G] [PreconnectedSpace G] [inst_4 : TopologicalSpace P] [ContinuousVAdd G P], ConnectedSpace P
An AddTorsor for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself.
- Defined in
- Mathlib.Topology.Algebra.MulAction
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddGroupstatement and proof · cited by 4,410
- AddTorsorstatement and proof · cited by 1,657
- PreconnectedSpacestatement and proof · cited by 64
- ContinuousVAddstatement and proof · cited by 52
- ConnectedSpacestatement · cited by 37
Cited by4
Results whose statement or proof uses this declaration.
- AffineSubspace.isConnected_setOfPred_sSameSideproof · cited by 3
- AffineSubspace.isConnected_setOfPred_sOppSideproof · cited by 2
- AffineSubspace.isConnected_setOfPred_wOppSideproof · cited by 2
- AffineSubspace.isConnected_setOfPred_wSameSideproof · cited by 2