Theorems · Theorem · logic and foundations
Subtype.mem
∀ {α : Type u_1} {s : Set α} (p : ↑s), ↑p ∈ sSee also Subtype.prop
- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Set.Elemstatement and proof · cited by 7,166
- Subtype.propproof · cited by 505
Cited by26
Results whose statement or proof uses this declaration.
- MeasureTheory.lpMeasSubgroupToLpTrim_ae_eqproof · cited by 6
- IntermediateField.le_iff_leproof · cited by 5
- MeasureTheory.lpMeas.aestronglyMeasurableproof · cited by 4
- MulAction.IwasawaStructure.commutator_leproof · cited by 4
- MeasureTheory.SimpleFunc.approxOn_memproof · cited by 3
- NumberField.hermiteTheorem.finite_of_finite_generating_setproof · cited by 2
- AntilipschitzWith.to_rightInvOn'proof · cited by 2
- IsCompact.extremePoints_nonemptyproof · cited by 2
- eq_of_linearIndepOn_id_of_span_subtypeproof · cited by 2
- Field.primitive_element_inf_auxproof · cited by 1
- CompactT2.ExtremallyDisconnected.projectiveproof · cited by 1
- IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_elementproof · cited by 1