Theorems · Theorem · general topology
IsLindelof.inter_right
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsClosed t → IsLindelof (s ∩ t)The intersection of a Lindelöf set and a closed set is a Lindelöf set.
- Defined in
- Mathlib.Topology.Compactness.Lindelof
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Filterproof · cited by 8,121
- IsClosedstatement and proof · cited by 1,639
- Filter.NeBotproof · cited by 853
- Filter.principalproof · cited by 740
- ClusterPtproof · cited by 138
- IsLindelofstatement and proof · cited by 85
- CountableInterFilterproof · cited by 78
- le_inf_iffproof · cited by 48
- ClusterPt.monoproof · cited by 30
- Filter.inf_principalproof · cited by 29
Cited by4
Results whose statement or proof uses this declaration.
- Topology.IsInducing.isLindelof_preimageproof · cited by 1
- IsLindelof.of_isClosed_subsetproof · cited by 1
- IsLindelof.diffproof · cited by 0
- IsLindelof.inter_leftproof · cited by 0