Theorems · Theorem · logic and foundations
Set.PairwiseDisjoint.subset
∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s t : Set ι} {f : ι → α},
t.PairwiseDisjoint f → s ⊆ t → s.PairwiseDisjoint f- Defined in
- Mathlib.Data.Set.Pairwise.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- PartialOrderOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- PartialOrderstatement and proof · cited by 6,410
- OrderBotstatement and proof · cited by 1,055
- Set.PairwiseDisjointstatement and proof · cited by 275
- Set.Pairwise.monoproof · cited by 55
Cited by8
Results whose statement or proof uses this declaration.
- Finset.card_dvd_card_image₂_rightproof · cited by 6
- Set.PairwiseDisjoint.countable_of_Iooproof · cited by 4
- MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variationproof · cited by 1
- Vitali.exists_disjoint_covering_aeproof · cited by 1
- exists_clopen_partition_of_clopen_coverproof · cited by 1
- Finset.card_le_card_biUnion_add_card_fiberproof · cited by 1
- AbsolutelyContinuousOnInterval.dist_le_of_pairwiseDisjoint_hasSumproof · cited by 1
- Finset.sum_card_sliceproof · cited by 0