Mathlib Map

Theorems · Theorem · order theory

Set.sUnion_eq_univ_iff

∀ {α : Type u_1} {c : Set (Set α)}, ⋃₀ c = Set.univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b
Defined in
Mathlib.Data.Set.Lattice
Cited by
8 results in Mathlib
Foundations
Depth 24 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds · cited by 6IsTopologicalBasis.of_has…MeasureTheory.Measure.ext_of_Ico' · cited by 2Measure.ext_of_Ico'Filter.isTopologicalBasis_Iic_principal · cited by 1Filter.isTopologicalBasis…MeasureTheory.Measure.ext_of_Icc' · cited by 1Measure.ext_of_Icc'Topology.IsLower.isTopologicalSpace_basis · cited by 1IsLower.isTopologicalSpac…Bornology.sUnion_bounded_univ · cited by 0Bornology.sUnion_bounded_…pi_generateFrom_eq_finite · cited by 0pi_generateFrom_eq_finiteSet.sUnion_finite_eq_univ · cited by 0Set.sUnion_finite_eq_univSet · cited by 53352SetSet.univ · cited by 3945Set.univSet.sUnion · cited by 392Set.sUnionSet.sUnion_eq_univ_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
  • Set.sUnionstatement · cited by 392

Cited by8

Results whose statement or proof uses this declaration.