Mathlib Map

Theorems · Theorem · order theory

Set.iUnion_eq_univ_iff

∀ {α : Type u_1} {ι : Sort u_5} {f : ι → Set α}, ⋃ i, f i = Set.univ ↔ ∀ (x : α), ∃ i, x ∈ f i
Defined in
Mathlib.Data.Set.Lattice
Cited by
19 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.

CompactExhaustion.exists_mem · cited by 5CompactExhaustion.exists_…Metric.iUnion_ball_nat · cited by 4Metric.iUnion_ball_natSet.iUnion_Iic · cited by 3Set.iUnion_Iicexists_mem_compactCovering · cited by 3exists_mem_compactCoveringMetric.iUnion_closedBall_nat · cited by 2Metric.iUnion_closedBall_…Set.iUnion_Ici · cited by 2Set.iUnion_IciSet.iUnion_Iio · cited by 2Set.iUnion_IioSet.iUnion_Ioi · cited by 2Set.iUnion_IoiTopologicalSpace.isTopologicalBasis_of_cover · cited by 2TopologicalSpace.isTopolo…IsOpen.iUnion_smul · cited by 1IsOpen.iUnion_smulIsOpen.iUnion_vadd · cited by 1IsOpen.iUnion_vaddMetric.iUnion_ball_nat_succ · cited by 1Metric.iUnion_ball_nat_su…DoubleCoset.iUnion_image_mk_leftRel · cited by 0DoubleCoset.iUnion_image_…DoubleCoset.iUnion_image_mk_rightRel · cited by 0DoubleCoset.iUnion_image_…IsOpen.iUnion_preimage_smul · cited by 0IsOpen.iUnion_preimage_sm…Set · cited by 53352SetSet.univ · cited by 3945Set.univSet.iUnion · cited by 2483Set.iUnionSet.iUnion_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.iUnionstatement · cited by 2,483

Cited by19

Results whose statement or proof uses this declaration.