extend_apply — Mathlib

English

Extend f g e' b equals g (f.symm b) for f : α ≃ β, g : α → γ, e' : β → γ, b : β.

Русский

Расширение along f для функций g и e' даёт значение g при аргументе b через обратную: extend f g e' b = g (f.symm b).

LaTeX

$$extend f g e' b = g (f.symm b)$$

Lean4

@[simp]
theorem extend_apply {f : α ≃ β} (g : α → γ) (e' : β → γ) (b : β) : extend f g e' b = g (f.symm b) := by
  rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]

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