Theorems · Theorem · order theory
Set.preimage_iUnion
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋃ i, s i = ⋃ i, f ⁻¹' s i- Defined in
- Mathlib.Data.Set.Lattice.Image
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.ofPredproof · cited by 6,101
- Set.preimagestatement · cited by 4,946
- Set.iUnionstatement · cited by 2,483
- Set.extproof · cited by 2,266
Cited by43
Results whose statement or proof uses this declaration.
- Set.preimage_iUnion₂proof · cited by 6
- AlgebraicGeometry.Scheme.Hom.preimage_iSupproof · cited by 4
- MeasureTheory.SigmaFinite.of_mapproof · cited by 4
- isClosedMap_iff_comap_nhds_leproof · cited by 3
- MeasureTheory.OuterMeasure.comap_iInfproof · cited by 3
- MeasureTheory.OuterMeasure.comap_ofFunctionproof · cited by 2
- measure_eq_measure_preimage_add_measure_tsum_Ico_zpowproof · cited by 2
- AntilipschitzWith.hausdorffMeasure_preimage_leproof · cited by 2
- PrimitiveSpectrum.hull_finsetInfproof · cited by 2
- AlgebraicGeometry.exists_appTop_π_eq_of_isLimitproof · cited by 2
- AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iffproof · cited by 2
- MeasureTheory.MeasurableSet.eq_preimage_restrict_countableproof · cited by 2