Mathlib Map

Theorems · Theorem · order theory

Set.image_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
41 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.image_iUnion₂ · cited by 11Set.image_iUnion₂nhdsSet_iUnion · cited by 10nhdsSet_iUnionSet.image2_iUnion_left · cited by 10Set.image2_iUnion_leftSet.image2_iUnion_right · cited by 10Set.image2_iUnion_rightIsSemilinearSet.image · cited by 9IsSemilinearSet.imageMeasureTheory.addHaar_image_le_mul_of_det_lt · cited by 4MeasureTheory.addHaar_ima…Set.smul_set_iUnion · cited by 4Set.smul_set_iUnionMeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe · cited by 4MeasurableSet.nullMeasura…TopologicalSpace.IsTopologicalBasis.isOpenMap_iff · cited by 4IsTopologicalBasis.isOpen…Set.vadd_set_iUnion · cited by 3Set.vadd_set_iUnionMeasurableEmbedding.sigmaFinite_map · cited by 3MeasurableEmbedding.sigma…HolderOnWith.hausdorffMeasure_image_le · cited by 2HolderOnWith.hausdorffMea…ChevalleyThm.chevalley_polynomialC · cited by 2ChevalleyThm.chevalley_po…MeasureTheory.OuterMeasure.map_iInf_comap · cited by 2OuterMeasure.map_iInf_com…IsCompactOpenCovered.of_iUnion_eq_of_finite · cited by 2IsCompactOpenCovered.of_i…Set · cited by 53352SetSet.image · cited by 5609Set.imageSet.iUnion · cited by 2483Set.iUnionSet.ext · cited by 2266Set.extSet.image_iUnionCITED BYCITES

Cites4

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.imagestatement · cited by 5,609
  • Set.iUnionstatement and proof · cited by 2,483
  • Set.extproof · cited by 2,266

Cited by41

Results whose statement or proof uses this declaration.