Theorems · Theorem · order theory
Function.Surjective.iUnion_comp
∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → ι₂},
Function.Surjective f → ∀ (g : ι₂ → Set α), ⋃ x, g (f x) = ⋃ y, g y- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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.iUnionstatement · cited by 2,483
- Function.Surjective.iSup_compproof · cited by 9
Cited by10
Results whose statement or proof uses this declaration.
- isSigmaCompact_iUnion_of_isCompactproof · cited by 2
- Set.dual_ordSeparatingSetproof · cited by 1
- IsCompactOpenCovered.exists_mem_of_isBasisproof · cited by 1
- ConnectedComponents.exists_fun_isClopen_of_infiniteproof · cited by 1
- Set.iUnion_unpair_prodproof · cited by 1
- MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnionproof · cited by 1
- approxAddOrderOf.vadd_eq_of_mul_dvdproof · cited by 1
- exists_clopen_partition_of_clopen_coverproof · cited by 1
- IsCountablySpanning.piproof · cited by 0
- approxOrderOf.smul_eq_of_mul_dvdproof · cited by 0