Theorems · Theorem · general topology
isOpen_compl_iff
∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen sᶜ ↔ IsClosed s- Defined in
- Mathlib.Topology.Basic
- Cited by
- 63 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- 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
- Compl.complstatement and proof · cited by 2,925
- IsOpenstatement and proof · cited by 2,400
- IsClosedstatement and proof · cited by 1,639
- IsClosed.isOpen_complproof · cited by 126
Cited by63
Results whose statement or proof uses this declaration.
- IsClosed.interproof · cited by 61
- isClosed_compl_iffproof · cited by 35
- IsClosed.monoproof · cited by 7
- Valued.isClosed_closedBallproof · cited by 4
- Valuation.isClosed_closedBallproof · cited by 4
- PrimeSpectrum.isClosed_iff_zeroLocusproof · cited by 4
- precise_refinement_setproof · cited by 3
- MeasureTheory.isClosed_setOfPred_preimage_ae_eqproof · cited by 3
- Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosedproof · cited by 3
- borel_eq_generateFrom_isClosedproof · cited by 3
- Urysohns.CU.continuous_limproof · cited by 3
- isClosed_range_inlproof · cited by 3