Theorems · Theorem · general topology
continuous_id_of_le
∀ {α : Type u} {t t' : TopologicalSpace α}, t ≤ t' → Continuous id- Defined in
- Mathlib.Topology.Order
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Continuousstatement · cited by 2,592
- continuous_id_iff_leproof · cited by 4
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.borel_eq_borel_of_leproof · cited by 2
- MeasurableSet.analyticSetproof · cited by 1
- t2Space_antitoneproof · cited by 0
- ContinuousLinearMap.toUniformConvergenceCLM_continuousproof · cited by 0