Mathlib Map

Theorems · Theorem · order theory

Set.image_empty

∀ {α : Type u_1} {β : Type u_2} (f : α → β), f '' ∅ = ∅
Defined in
Mathlib.Data.Set.Image
Cited by
73 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.smul_set_empty · cited by 19Set.smul_set_emptyAffineSubspace.map_span · cited by 16AffineSubspace.map_spanAffineSubspace.map_bot · cited by 7AffineSubspace.map_botSet.vadd_set_empty · cited by 5Set.vadd_set_emptyNNReal.coe_sInf · cited by 5NNReal.coe_sInfNNReal.coe_sSup · cited by 5NNReal.coe_sSupDisjoint.image · cited by 4Disjoint.imageIdeal.span_pow_eq_top · cited by 4Ideal.span_pow_eq_topMeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe · cited by 4MeasurableSet.nullMeasura…MonotoneOn.map_sSup_of_continuousWithinAt · cited by 3MonotoneOn.map_sSup_of_co…isOpenMap_eval · cited by 3isOpenMap_evalMonotoneOn.tendsto_nhdsLT · cited by 3MonotoneOn.tendsto_nhdsLTFinsupp.lmapDomain_supported · cited by 2Finsupp.lmapDomain_suppor…HolderOnWith.hausdorffMeasure_image_le · cited by 2HolderOnWith.hausdorffMea…IsClosedMap.of_nonempty · cited by 2IsClosedMap.of_nonemptySet · cited by 53352SetSet.image · cited by 5609Set.imageSet.image_emptyCITED BYCITES

Cites2

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

  • Setstatement · cited by 53,352
  • Set.imagestatement · cited by 5,609

Cited by73

Results whose statement or proof uses this declaration.