congrRight — Mathlib

English

Given an equivalence e: Y ≃ Z, there is an equivalence between LocallyConstant X Y and LocallyConstant X Z, transported via map e.

Русский

Дано эквивалентность e: Y ≃ Z, существует эквивалентность между LocallyConstant X Y и LocallyConstant X Z через отображение map e.

LaTeX

$$$ \\text{congrRight } (e) : LocallyConstant X Y \\simeq LocallyConstant X Z $$$

Lean4

/-- The equivalence between `LocallyConstant X Y` and `LocallyConstant X Z` given an
equivalence `Y ≃ Z`
-/
@[simps]
def congrRight (e : Y ≃ Z) : LocallyConstant X Y ≃ LocallyConstant X Z
    where
  toFun := map e
  invFun := map e.symm
  left_inv := by intro; ext; simp
  right_inv := by intro; ext; simp

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