Theorems · Theorem · order theory
SetLike.ext_iff
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q- Defined in
- Mathlib.Data.SetLike.Basic
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext, Quot.sound
- Assumes
- SetLike
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.
- SetLikestatement and proof · cited by 1,084
- SetLike.coe_injectiveproof · cited by 374
- Set.ext_iffproof · cited by 90
Cited by64
Results whose statement or proof uses this declaration.
- LinearMap.exact_iffproof · cited by 27
- Finsupp.mem_span_iff_linearCombinationproof · cited by 7
- Subalgebra.map_injectiveproof · cited by 5
- Polynomial.Gal.extproof · cited by 5
- AddSubmonoid.eq_bot_iff_forallproof · cited by 4
- AddMonoidHom.exists_mrange_eq_mgraphproof · cited by 4
- AddSubgroup.addSubgroupOf_injproof · cited by 3
- Subalgebra.toSubmodule_injectiveproof · cited by 3
- Submonoid.eq_bot_iff_forallproof · cited by 3
- LinearMap.localized'_ker_eq_ker_localizedMapproof · cited by 3
- KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChangeproof · cited by 3
- Submodule.toAddSubgroup_injectiveproof · cited by 2