arrowCongr — Mathlib

English

If e1 : α1 ≃ α2 and e2 : β1 ≃ β2, then α1 → β1 ≃ α2 → β2.

Русский

Если e1: α1 ≃ α2 и e2: β1 ≃ β2, то функции α1 → β1 эквивалентны α2 → β2.

LaTeX

$$$\text{arrowCongr } e1 e2 : (α1 \to β1) \simeq (α2 \to β2)$$$

Lean4

/-- If `α₁` is equivalent to `α₂` and `β₁` is equivalent to `β₂`, then the type of maps `α₁ → β₁`
is equivalent to the type of maps `α₂ → β₂`. -/
@[simps (attr := grind =) apply]
def arrowCongr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂)
    where
  toFun f := e₂ ∘ f ∘ e₁.symm
  invFun f := e₂.symm ∘ f ∘ e₁
  left_inv f := by grind
  right_inv f := by grind

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