Mathlib Map

Theorems · Definition · order theory

Set.codRestrict

{α : Type u_1} → {ι : Sort u_5} → (f : ι → α) → (s : Set α) → (∀ (x : ι), f x ∈ s) → ι → ↑s

Restrict codomain of a function f to a set s. Same as Subtype.coind but this version has codomain ↥s instead of Subtype s.

Defined in
Mathlib.Data.Set.Restrict
Cited by
48 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.

Real.expOrderIso · cited by 12Real.expOrderIsoContinuous.codRestrict · cited by 11Continuous.codRestrictSet.injective_codRestrict · cited by 10Set.injective_codRestrictTopology.IsEmbedding.aestronglyMeasurable_comp_iff · cited by 6IsEmbedding.aestronglyMea…Function.Injective.codRestrict · cited by 5Injective.codRestrictcfc_comp · cited by 5cfc_compSet.not_injOn_infinite_finite_image · cited by 4Set.not_injOn_infinite_fi…cfcₙ_comp · cited by 3cfcₙ_compContinuousAt.codRestrict · cited by 3ContinuousAt.codRestrictAlgebraicIndependent.map · cited by 3AlgebraicIndependent.mapTopology.IsEmbedding.codRestrict · cited by 3IsEmbedding.codRestrictEquiv.Perm.exists_extending_pair · cited by 2Perm.exists_extending_pairSet.domRestrict_comp_codRestrict · cited by 2Set.domRestrict_comp_codR…isAddFundamentalDomain_Ioc' · cited by 2isAddFundamentalDomain_Io…Set.range_codRestrict · cited by 2Set.range_codRestrictSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemSet.codRestrictCITED BYCITES

Cites2

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.Elemstatement · cited by 7,166

Cited by51

Results whose statement or proof uses this declaration.