Mathlib Map

Theorems · Theorem · logic and foundations

Set.mem_range_self

∀ {α : Type u} {ι : Sort u_1} {f : ι → α} (i : ι), f i ∈ Set.range f
Defined in
Mathlib.Data.Set.Operations
Cited by
328 results in Mathlib
Foundations
Depth 4 from the axioms, rests on 11 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

le_ciSup · cited by 57le_ciSupSet.rangeFactorization · cited by 56Set.rangeFactorizationSet.preimage_range · cited by 38Set.preimage_rangeFinsupp.range_linearCombination · cited by 24Finsupp.range_linearCombi…Topology.IsOpenEmbedding.map_nhds_eq · cited by 22IsOpenEmbedding.map_nhds_…ContMDiffWithinAt.comp · cited by 18ContMDiffWithinAt.compuniqueMDiffWithinAt_univ · cited by 14uniqueMDiffWithinAt_univaffineCombination_mem_affineSpan · cited by 12affineCombination_mem_aff…stronglyMeasurable_of_tendsto · cited by 12stronglyMeasurable_of_ten…Affine.Simplex.dist_circumcenter_eq_circumradius · cited by 12Simplex.dist_circumcenter…Function.Exact.apply_apply_eq_zero · cited by 11Exact.apply_apply_eq_zeroMeasureTheory.StronglyMeasurable.isSeparable_range · cited by 10StronglyMeasurable.isSepa…Set.isCompl_range_inl_range_inr · cited by 9Set.isCompl_range_inl_ran…Module.Basis.span_apply · cited by 8Basis.span_applyisLUB_of_tendsto_atTop · cited by 7isLUB_of_tendsto_atTopSet · cited by 53352SetSet.range · cited by 4705Set.rangeSet.mem_range_selfCITED 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.rangestatement · cited by 4,705

Cited by329

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 329.