restrict_extend_compl_range — Mathlib

English

Restriction to the complement of the range of extend f g g' equals g' composed with the projection to the original domain.

Русский

Ограничение дополнения к диапазону extend даёт функцию g' после проекции на исходную область.

LaTeX

$$$(\\operatorname{range} f)^{c}.restrict (\\operatorname{extend} f g g') = g' \\circ \\operatorname{Subtype.val}$$$

Lean4

@[simp]
theorem restrict_extend_compl_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val := by classical exact restrict_dite_compl _ _

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