Mathlib Map

Theorems · Theorem · order theory

SetLike.ext

∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (∀ (x : B), x ∈ p ↔ x ∈ q) → p = q

Note: implementers of SetLike must copy this lemma in order to tag it with @[ext].

Defined in
Mathlib.Data.SetLike.Basic
Cited by
92 results in Mathlib
Foundations
Depth 6 from the axioms · uses propext, Quot.sound
Assumes
SetLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.ext · cited by 565Finset.extSubmodule.ext · cited by 204Submodule.extSubgroup.ext · cited by 108Subgroup.extAddSubgroup.ext · cited by 75AddSubgroup.extSubmonoid.ext · cited by 48Submonoid.extAddSubmonoid.ext · cited by 32AddSubmonoid.extSubalgebra.ext · cited by 28Subalgebra.extLieSubmodule.ext · cited by 20LieSubmodule.extFunction.Exact.linearMap_ker_eq · cited by 18Exact.linearMap_ker_eqIntermediateField.ext · cited by 17IntermediateField.extAffineSubspace.ext · cited by 16AffineSubspace.extFractionalIdeal.ext · cited by 13FractionalIdeal.extPointedCone.ext · cited by 13PointedCone.extProperCone.ext · cited by 12ProperCone.extSubring.ext · cited by 9Subring.extSet.ext · cited by 2266Set.extSetLike · cited by 1084SetLikeSetLike.coe_injective · cited by 374SetLike.coe_injectiveSetLike.extCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by92

Results whose statement or proof uses this declaration.