Theorems · Theorem · general topology
Inseparable.specializes
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → x ⤳ y- Defined in
- Mathlib.Topology.Inseparable
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Eq.leproof · cited by 605
- Specializesstatement · cited by 176
- Inseparablestatement and proof · cited by 160
Cited by16
Results whose statement or proof uses this declaration.
- t1Space_TFAEproof · cited by 8
- specializes_iff_inseparableproof · cited by 5
- AlgebraicGeometry.spread_out_of_isGermInjective'proof · cited by 3
- Inseparable.map_of_continuousWithinAtproof · cited by 2
- AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrictproof · cited by 2
- r1Space_iff_inseparable_or_disjoint_nhdsproof · cited by 1
- AlgebraicGeometry.spread_out_of_isGermInjectivestatement and proof · cited by 1
- AlgebraicGeometry.spread_out_unique_of_isGermInjectivestatement and proof · cited by 1
- AlgebraicGeometry.spread_out_unique_of_isGermInjective'proof · cited by 1
- Inseparable.joinedInproof · cited by 0
- Inseparable.nsmulproof · cited by 0
- Inseparable.powproof · cited by 0