equivSucc — Mathlib

English

The equivalence between successive embeddings extends to include a corresponding top-like coordinate in the target closure.

Русский

Эквивалентность последовательных вложений расширяется за счет добавления координаты верхнего типа в целевом замыкании.

LaTeX

$$$$equivSucc_i: (E⟮

Lean4

/-- Extend `succEquiv` from `ι` to `WithTop ι`. -/
def equivSucc (i : WithTop ι) : (E⟮<i⁺⟯ →ₐ[F] Ē) ≃ (E⟮<i⟯ →ₐ[F] Ē) × factor i :=
  i.recTopCoe (((equivOfEq <| by rw [succ_top]).arrowCongr .refl).trans <| .symm <| .prodPUnit _) (succEquiv ·)

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