Theorems · Theorem · order theory
Disjoint.subset_compl_right
∀ {α : Type u_1} {s t : Set α}, Disjoint s t → s ⊆ tᶜAlias of the reverse direction of Set.subset_compl_iff_disjoint_right.
- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Compl.complstatement · cited by 2,925
- Disjointstatement · cited by 2,201
- Set.subset_compl_iff_disjoint_rightproof · cited by 17
Cited by15
Results whose statement or proof uses this declaration.
- Disjoint.closure_leftproof · cited by 6
- codiscreteWithin_iff_locallyEmptyComplementWithinproof · cited by 3
- isClopen_inter_of_disjoint_cover_clopenproof · cited by 3
- Topology.IsCoinducing.isConnected_preimage_of_isClosedproof · cited by 3
- MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subsetproof · cited by 2
- ContinuousMap.idealOfSet_ofIdeal_eq_closureproof · cited by 2
- Metric.ball_infDist_subset_complproof · cited by 2
- exists_tsupport_one_of_isOpen_isClosedproof · cited by 2
- IsCompact.exists_isOpen_closure_subsetproof · cited by 1
- MeasureTheory.Measure.nonempty_inter_support_of_posproof · cited by 1
- Circle.compl_path_image_Iocproof · cited by 1
- Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisorsproof · cited by 1