update_comp_equiv — Mathlib

English

If β is unique, then Unique α is equivalent to α ≃ β.

Русский

Если β уникален, то Unique α эквивалентно α ≃ β.

LaTeX

$$$Unique\\alpha\\ \\simeq\\ (\\alpha\\simeq\\beta)\\quad[Unique\\beta].$$$

Lean4

theorem update_comp_equiv [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) :
    update f a v ∘ g = update (f ∘ g) (g.symm a) v := by
  rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]

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