eq_mp_bijective — Mathlib

English

If α = β, then the map h ↦ h mp is bijective between α and β; concretely, Eq.mp h is a bijection.

Русский

Если α = β, то отображение h ↦ h.mp является биективным между α и β; конкретно, Eq.mp h — биекция.

LaTeX

$$$ \forall {\alpha \beta} (h : \alpha = \beta),\; \operatorname{Bijective} (h .mp)$$$

Lean4

theorem eq_mp_bijective {α β : Sort _} (h : α = β) : Function.Bijective (Eq.mp h) := by
  -- TODO: mathlib3 uses `eq_rec_on_bijective`, difference in elaboration here
    -- due to `@[macro_inline]` possibly?

  cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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