Mathlib Map

Theorems · Theorem · logic and foundations

Set.left_eq_inter

∀ {α : Type u} {s t : Set α}, s = s ∩ t ↔ s ⊆ t
Defined in
Mathlib.Data.Set.Basic
Cited by
4 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.sep_eq_inter_sep · cited by 2Set.sep_eq_inter_sepSeparatedNhds.isClosed_left_of_isClosed_union · cited by 2SeparatedNhds.isClosed_le…isDiscrete_iff_forall_mem_exists_isClosed · cited by 1isDiscrete_iff_forall_mem…Equidecomp.IsDecompOn.comp · cited by 0IsDecompOn.compSet · cited by 53352Setleft_eq_inf · cited by 4left_eq_infSet.left_eq_interCITED BYCITES

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
  • left_eq_infproof · cited by 4

Cited by4

Results whose statement or proof uses this declaration.