Theorems · Definition · Lie groups
Homeomorph.neg
(G : Type u_1) → [inst : TopologicalSpace G] → [inst_1 : InvolutiveNeg G] → [ContinuousNeg G] → G ≃ₜ G
Negation in a topological group as a homeomorphism.
- Defined in
- Mathlib.Topology.Algebra.Group.Basic
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
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
- Equiv.Permproof · cited by 1,375
- Homeomorphstatement · cited by 725
- InvolutiveNegstatement and proof · cited by 151
- ContinuousNegstatement and proof · cited by 119
- Equiv.negproof · cited by 53
Cited by24
Results whose statement or proof uses this declaration.
- tsum_negproof · cited by 5
- integrable_rpow_mul_exp_neg_mul_sqproof · cited by 2
- HasCompactSupport.convolutionExistsAtproof · cited by 2
- neg_closureproof · cited by 2
- integral_comp_absproof · cited by 2
- integral_comp_neg_Iicproof · cited by 2
- isOpenMap_negproof · cited by 1
- MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iicproof · cited by 1
- nhds_zero_symm'proof · cited by 1
- continuous_neg_iffproof · cited by 1
- continuousAt_neg_iffproof · cited by 1