optionCongr_trans — Mathlib

English

Composition of equivalences respects optionCongr: optionCongr (e1.trans e2) equals (optionCongr e1).trans (optionCongr e2).

Русский

Суммирование эквивалентностей в отношении Option сохраняется: optionCongr (e1.trans e2) = (optionCongr e1).trans (optionCongr e2).

LaTeX

$$$\\text{optionCongr}(e_1\\,\\text{trans } e_2) = (\\text{optionCongr } e_1).\\text{trans } (\\text{optionCongr } e_2).$$$

Lean4

@[simp]
theorem optionCongr_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
    optionCongr (e₁.trans e₂) = (optionCongr e₁).trans (optionCongr e₂) :=
  by
  ext x : 1
  symm
  apply Option.map_map

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