English
Embeddings whose range lies within a set bs are equivalent to embeddings into bs.
Русский
Встраивания, образ которых лежит в bs, эквивалентны вложениям в bs.
LaTeX
$$$\\{ f : \\alpha \\hookrightarrow \\beta \\;\\text{with} \\; \\forall a, f(a) \\in bs \\} \\cong (\\alpha \\hookrightarrow bs.Elem)$$$
Lean4
/-- Embeddings whose range lies within a set are equivalent to embeddings to that set.
This is `Function.Embedding.codRestrict` as an equiv. -/
def codRestrict (α : Type*) {β : Type*} (bs : Set β) : { f : α ↪ β // ∀ a, f a ∈ bs } ≃ (α ↪ bs)
where
toFun f := (f : α ↪ β).codRestrict bs f.prop
invFun f := ⟨f.trans (Function.Embedding.subtype _), fun a => (f a).prop⟩
