Theorems · Theorem · general topology
IrreducibleSpace.isIrreducible_univ
∀ (X : Type u_3) [inst : TopologicalSpace X] [IrreducibleSpace X], IsIrreducible Set.univ
- Defined in
- Mathlib.Topology.Irreducible
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 8 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
- Set.univstatement · cited by 3,945
- IsIrreduciblestatement · cited by 59
- IrreducibleSpacestatement and proof · cited by 40
- Set.univ_nonemptyproof · cited by 21
- PreirreducibleSpace.isPreirreducible_univproof · cited by 7
Cited by8
Results whose statement or proof uses this declaration.
- genericPointproof · cited by 15
- genericPoint_specproof · cited by 7
- AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpaceproof · cited by 2
- irreducibleComponents_eq_singletonproof · cited by 2
- AlgebraicGeometry.Scheme.Hom.isIrreducible_preimageproof · cited by 1
- irreducibleSpace_defproof · cited by 0
- genericPoint_specializesproof · cited by 0