of_codRestrict — Mathlib

English

If f: X → Y and t ⊆ Y with ht: ∀ x, f(x) ∈ t, and IsInducing (t.codRestrict f ht), then IsInducing f.

Русский

Пусть f: X → Y и т ⊆ Y с ht: для всех x выполняется f(x) ∈ t; если IsInducing (t.codRestrict f ht), тогда IsInducing f.

LaTeX

$$$$ \\text{If } ht: \\forall x, f(x) \\in t \\text{ and } IsInducing(t\\,\\text{codRestrict } f ht) \\,\\text{then } IsInducing f. $$$$

Lean4

theorem of_codRestrict {f : X → Y} {t : Set Y} (ht : ∀ x, f x ∈ t) (h : IsInducing (t.codRestrict f ht)) :
    IsInducing f :=
  subtypeVal.comp h

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