Mathlib Map

Theorems · Theorem · logic and foundations

Set.univ_subset_iff

∀ {α : Type u} {s : Set α}, Set.univ ⊆ s ↔ s = Set.univ
Defined in
Mathlib.Data.Set.Basic
Cited by
49 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.eq_univ_iff_forall · cited by 93Set.eq_univ_iff_forallSet.eq_univ_of_univ_subset · cited by 7Set.eq_univ_of_univ_subsetatBot_le_cocompact · cited by 4atBot_le_cocompactSet.preimage_eq_univ_iff · cited by 4Set.preimage_eq_univ_iffcountable_cover_nhds_of_sigmaCompact · cited by 3countable_cover_nhds_of_s…AlgebraicGeometry.IsDominant.of_comp · cited by 3IsDominant.of_compAddSubgroup.leftCoset_cover_const_iff_surjOn · cited by 3AddSubgroup.leftCoset_cov…RingHom.Smooth.ofLocalizationSpanTarget · cited by 2Smooth.ofLocalizationSpan…MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul · cited by 1IsPreprimitive.exists_mem…interior_eq_univ · cited by 1interior_eq_univPrimeSpectrum.zeroLocus_eq_univ_iff · cited by 1PrimeSpectrum.zeroLocus_e…countable_cover_nhds_interior · cited by 1countable_cover_nhds_inte…finite_cover_nhds_interior · cited by 1finite_cover_nhds_interiorFilter.add_top_of_nonneg · cited by 1Filter.add_top_of_nonnegMeasureTheory.Measure.OuterRegular.of_restrict · cited by 1OuterRegular.of_restrictSet · cited by 53352SetSet.univ · cited by 3945Set.univtop_le_iff · cited by 175top_le_iffSet.univ_subset_iffCITED BYCITES

Cites3

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.univstatement · cited by 3,945
  • top_le_iffproof · cited by 175

Cited by49

Results whose statement or proof uses this declaration.