apply_extend — Mathlib

English

For any F, extend f g e' b after applying a function F to the result equals extend f (F ∘ g) (F ∘ e') b.

Русский

Пусть F — функция, тогда F применяем к Extend даёт Extend с композициями F∘g и F∘e'.

LaTeX

$$$\,F(\operatorname{extend} f g e' b) = \operatorname{extend} f (F \circ g) (F \circ e') b$$$

Lean4

theorem apply_extend {δ} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β) :
    F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
  open scoped Classical in apply_dite F _ _ _

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