Theorems · Theorem · order theory
Eq.trans_subset
∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LE α], a = b → b ⊆ c → a ⊆ cSet notation form of Eq.trans_le
- Defined in
- Mathlib.Order.RelClasses
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- UsesSetNotationForOrderLE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Eq.trans_leproof · cited by 155
Cited by16
Results whose statement or proof uses this declaration.
- Finset.card_dvd_card_image₂_rightproof · cited by 6
- MulAction.IsBlock.disjoint_smul_set_smulproof · cited by 2
- AddAction.IsBlock.disjoint_vadd_set_vaddproof · cited by 2
- ContinuousOn.preimage_mem_nhdsSetWithinproof · cited by 2
- interior_union_inter_interior_compl_left_subsetproof · cited by 1
- interior_union_inter_interior_compl_right_subsetproof · cited by 1
- Matroid.setOfPred_dual_isBase_eqproof · cited by 1
- HasFTaylorSeriesUpTo.tsupport_monoproof · cited by 1
- mem_nhdsSet_inducedproof · cited by 1
- contDiffOn_fderiv_coord_changeproof · cited by 1
- Continuous.exists_lift_sigmaproof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocusproof · cited by 0