Mathlib Map

Theorems · Theorem · order theory

Set.preimage_univ

∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univ
Defined in
Mathlib.Data.Set.Image
Cited by
46 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

OpenPartialHomeomorph.extend_source · cited by 17OpenPartialHomeomorph.ext…MeasureTheory.Measure.fst_map_prodMk₀ · cited by 9Measure.fst_map_prodMk₀contMDiffAt_iff · cited by 7contMDiffAt_iffAlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace · cited by 7QuasiCompact.compactSpace…ContDiffAt.fderiv · cited by 6ContDiffAt.fderivAlgebraicGeometry.IsOpenImmersion.range_pullbackFst · cited by 4IsOpenImmersion.range_pul…AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd · cited by 4IsOpenImmersion.range_pul…Seminorm.convex_ball · cited by 4Seminorm.convex_ballMeasureTheory.SigmaFinite.of_map · cited by 4SigmaFinite.of_mapMeasureTheory.Measure.snd_map_prodMk₀ · cited by 3Measure.snd_map_prodMk₀ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib' · cited by 3ProbabilityTheory.condExp…MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk · cited by 3AEStronglyMeasurable.comp…MeasureTheory.cylinder_univ · cited by 2MeasureTheory.cylinder_un…MeasureTheory.Measure.isFiniteMeasure_of_map · cited by 2Measure.isFiniteMeasure_o…AddMonoidHom.measurePreserving · cited by 2AddMonoidHom.measurePrese…Set · cited by 53352SetSet.preimage · cited by 4946Set.preimageSet.univ · cited by 3945Set.univSet.preimage_univCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by46

Results whose statement or proof uses this declaration.