rangeFactorization_eq

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.rangeFactorization_eq

English

For any f : ι → β, the projection of rangeFactorization f equals f.

Русский

Для функции f: ι → β проекция rangeFactorization f возвращает исходную функцию.

LaTeX

$$$$ \\operatorname{Subtype.val} \\circ \\operatorname{rangeFactorization} f = f $$$$

Lean4

theorem rangeFactorization_eq {f : ι → β} : Subtype.val ∘ rangeFactorization f = f :=
  funext fun _ => rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru