codRestrict — Mathlib

English

If e: X → Y is an inducing map, then the codomain-restricted map Set.codRestrict e s hs is also inducing, provided hs holds.

Русский

Если e: X → Y — индуцирующее отображение, то ограничение кодом e на s является индуцирующим отображением при условии hs.

LaTeX

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

Lean4

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

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