imageFactorization_eq — Mathlib

English

The mapping Subtype.val ∘ imageFactorization f s equals f ∘ Subtype.val; i.e., the factorization is compatible with f on s.

Русский

Отображение Subtype.val ∘ imageFactorization f s эквивалентно f ∘ Subtype.val; факторизация совместима с f на s.

LaTeX

$$$\\operatorname{Subtype.val} \\circ \\operatorname{imageFactorization} f s = f \\circ \\operatorname{Subtype.val}$$$

Lean4

theorem imageFactorization_eq {f : α → β} {s : Set α} : Subtype.val ∘ imageFactorization f s = f ∘ Subtype.val :=
  funext fun _ => rfl

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