Mathlib Map

Theorems · Theorem · order theory

SetLike.mem_coe

∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
Defined in
Mathlib.Data.SetLike.Basic
Cited by
302 results in Mathlib
Foundations
Depth 5 from the axioms, rests on 10 definitions · uses no axioms
Assumes
SetLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finsupp.range_linearCombination · cited by 24Finsupp.range_linearCombi…Submodule.span_singleton_le_iff_mem · cited by 21Submodule.span_singleton_…LieSubalgebra.subset_lieSpan · cited by 19LieSubalgebra.subset_lieS…Subgroup.le_normalizer · cited by 19Subgroup.le_normalizerTopologicalSpace.Opens.mem_iSup · cited by 17Opens.mem_iSupLieSubmodule.subset_lieSpan · cited by 14LieSubmodule.subset_lieSp…Submodule.mem_iInf · cited by 12Submodule.mem_iInfFinset.sum_of_injOn · cited by 8Finset.sum_of_injOnlowerClosure_singleton · cited by 8lowerClosure_singletonAddSubgroup.zmultiples_le · cited by 7AddSubgroup.zmultiples_leSubmodule.mem_iSup_of_directed · cited by 7Submodule.mem_iSup_of_dir…vectorSpan_eq_span_vsub_set_right · cited by 7vectorSpan_eq_span_vsub_s…Subgroup.zpowers_le · cited by 6Subgroup.zpowers_leAddSubgroup.le_normalizer · cited by 6AddSubgroup.le_normalizerTwoSidedIdeal.mem_span_iff · cited by 6TwoSidedIdeal.mem_span_iffSet · cited by 53352SetSetLike.coe · cited by 8199SetLike.coeSetLike · cited by 1084SetLikeSetLike.mem_coeCITED BYCITES

Cites3

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 · cited by 8,199
  • SetLikestatement and proof · cited by 1,084

Cited by302

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 302.