Theorems · Theorem · logic and foundations

Set.Subset.antisymm

∀ {α : Type u} {a b : Set α}, a ⊆ b → b ⊆ a → a = b

Defined in: Mathlib.Data.Set.Basic
Cited by: 213 results in Mathlib
Foundations: Depth 6 from the axioms, rests on 15 definitions · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites2

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.extproof · cited by 2,266

Cited by213

Results whose statement or proof uses this declaration.

IsClosed.closure_eqproof · cited by 139
Set.preimage_image_eqproof · cited by 87
Set.image_preimage_eqproof · cited by 38
Set.image_eq_preimage_of_inverseproof · cited by 27
Set.image_sdiffproof · cited by 24
Set.InjOn.image_iInter_eqproof · cited by 22
closure_Iooproof · cited by 20
closure_ballproof · cited by 20
Set.sdiff_union_of_subsetproof · cited by 18
Set.eq_of_subset_of_subsetproof · cited by 11
Set.center_eq_univproof · cited by 10
Set.centralizer_univproof · cited by 10

Showing the 200 most cited of 213.