Theorems · Theorem · general topology
IsClosed.union
∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)- Defined in
- Mathlib.Topology.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 58 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.
Cites6
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
- IsOpenproof · cited by 2,400
- IsClosedstatement · cited by 1,639
- IsOpen.interproof · cited by 98
- Set.compl_unionproof · cited by 30
Cited by17
Results whose statement or proof uses this declaration.
- Filter.hasBasis_coclosedCompactproof · cited by 8
- nhdsNE_of_nhdsNE_sdiff_finiteproof · cited by 3
- MeasureTheory.measure_univ_of_isAddLeftInvariantproof · cited by 2
- isClosed_impproof · cited by 2
- hasBasis_coclosedLindelofproof · cited by 2
- dist_integral_mulExpNegMulSq_comp_leproof · cited by 1
- MeasureTheory.measure_univ_of_isMulLeftInvariantproof · cited by 1
- CompactT2.Projective.extremallyDisconnectedproof · cited by 1
- isClosedMap_sumproof · cited by 1
- isClosed_preCantorSetproof · cited by 1