Theorems · Theorem · order theory
SetLike.coe_ssubset_coe
∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B] {S T : A},
↑S ⊂ ↑T ↔ S < T- Defined in
- Mathlib.Data.SetLike.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- SetLike.coestatement and proof · cited by 8,199
- PartialOrderstatement and proof · cited by 6,410
- SetLikestatement and proof · cited by 1,084
- SetLike.coe_subset_coeproof · cited by 53
- lt_iff_le_and_neproof · cited by 47
- IsConcreteLEstatement and proof · cited by 28
- ssubset_iff_subset_neproof · cited by 7
- SetLike.coe_ne_coeproof · cited by 6
Cited by5
Results whose statement or proof uses this declaration.
- ArchimedeanClass.addSubgroup_strictAntiOnproof · cited by 1
- MulArchimedeanClass.subgroup_strictAntiOnproof · cited by 1
- ArchimedeanClass.subsemigroup_strictAntiproof · cited by 1
- MulArchimedeanClass.subsemigroup_strictAntiproof · cited by 1
- SetLike.coe_strictMonoproof · cited by 0