Theorems · Theorem · general topology
IsCompact.inter_right
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsClosed t → IsCompact (s ∩ t)The intersection of a compact set and a closed set is a compact set.
- Defined in
- Mathlib.Topology.Compactness.Compact
- Cited by
- 30 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.
Cites14
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
- IsCompactstatement and proof · cited by 1,282
- le_transproof · cited by 985
- Filter.NeBotproof · cited by 853
- Filter.principalproof · cited by 740
- Set.inter_subset_leftproof · cited by 360
- Set.inter_subset_rightproof · cited by 329
- ClusterPtproof · cited by 138
- Filter.le_principal_iffproof · cited by 87
Cited by30
Results whose statement or proof uses this declaration.
- IsCompact.of_isClosed_subsetproof · cited by 67
- IsCompact.diffproof · cited by 8
- IsCompact.inter_leftproof · cited by 7
- ModelWithCorners.locallyCompactSpaceproof · cited by 5
- Topology.IsInducing.locallyCompactSpaceproof · cited by 4
- Metric.finite_isBounded_inter_isClosedproof · cited by 4
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_setproof · cited by 3
- isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_leproof · cited by 2
- SmoothBumpFunction.isCompact_symm_image_closedBallproof · cited by 2
- exists_subset_nhds_of_isCompact'proof · cited by 2
- ContinuousOn.exists_isMinOn'proof · cited by 2
- LowerSemicontinuousOn.isCompact_inter_preimage_Iicproof · cited by 2