codRestrict — Mathlib

English

If e is an embedding, then the codomain-restricted map Set.codRestrict e s hs is an embedding.

Русский

Если e — вложение, то ограничение кодом Set.codRestrict e s hs также является вложением.

LaTeX

$$$\\forall e:X\\to Y,\\; \\text{IsEmbedding}(e) \\Rightarrow \\forall s\\subseteq Y,\\; (\\forall x, e(x)\\in s) \\Rightarrow \\text{IsEmbedding}\\left(\\text{codRestrict } e s hs\\right).$$$

Lean4

protected theorem codRestrict {e : X → Y} (he : IsEmbedding e) (s : Set Y) (hs : ∀ x, e x ∈ s) :
    IsEmbedding (codRestrict e s hs) :=
  he.of_comp (he.continuous.codRestrict hs) continuous_subtype_val

Похожие утверждения