restrict_comp_codRestrict — Mathlib

English

Restricting after codRestrict equals restricting after the original map: restricting g after codRestrict f is the same as restricting g after f.

Русский

Ограничение после codRestrict равно ограничению после исходной функции.

LaTeX

$$$b.restrict g \\circ b.codRestrict f h = g \\circ f$$$

Lean4

@[simp]
theorem restrict_comp_codRestrict {f : ι → α} {g : α → β} {b : Set α} (h : ∀ x, f x ∈ b) :
    b.restrict g ∘ b.codRestrict f h = g ∘ f :=
  rfl

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