restrict_extend_range — Mathlib

English

The restriction of the range of f to extend f g g' equals the function that sends each x in range f to g at a chosen preimage of x.

Русский

Ограничение диапазона функции extend по range f равняется функции, отправляющей каждую x из range f в g(выборка) по произвольному предобразу x.

LaTeX

$$$(\\operatorname{range} f)\\restrict (\\operatorname{extend} f g g') = x \\mapsto g(\\text{choose } a \\,:\\, f a = x)$$$

Lean4

theorem restrict_extend_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f).restrict (extend f g g') = fun x => g x.coe_prop.choose := by classical exact restrict_dite _ _

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