Theorems · Theorem · Lie groups
IsOpen.add_right
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α},
IsOpen s → IsOpen (s + t)- Defined in
- Mathlib.Topology.Algebra.Group.Pointwise
- 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- AddGroupstatement and proof · cited by 4,410
- IsOpenstatement and proof · cited by 2,400
- AddOppositestatement and proof · cited by 452
- Set.addstatement · cited by 338
- ContinuousConstVAddstatement and proof · cited by 97
- IsOpen.vadd_leftproof · cited by 3
- Set.image_op_vaddproof · cited by 2
Cited by4
Results whose statement or proof uses this declaration.
- subset_interior_add_leftproof · cited by 4
- IsOpen.add_closureproof · cited by 3
- MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariantproof · cited by 1
- Convex.exists_subset_interior_convexHull_finset_of_isCompactproof · cited by 0