piEquivSucc — Mathlib

English

One-step extension of a family of bijections to piLT by adding one step in a succ-ordered index.

Русский

Добавление одного шага к биекциям в piLT через succ-индекс.

LaTeX

$$$\\mathrm{piEquivSucc}\\; (equiv)\\; (e)\\; (hi) : \\text{new equivalence on } F(\\mathrm{Order.succ} i)$$$

Lean4

/-- Extend a family of bijections to `piLT` by one step. -/
def piEquivSucc : ∀ j : Iic i⁺, F j ≃ piLT X j :=
  piSplitLE (X := fun i ↦ F i ≃ piLT X i)
    (fun j ↦ equiv ⟨j, (lt_succ_iff_of_not_isMax hi).mp j.2⟩,
      e.trans <|
        ((equiv ⟨i, le_rfl⟩).prodCongr <| Equiv.refl _).trans <|
          piSplitLE.trans <| Equiv.piCongrSet <| Set.ext fun _ ↦ (lt_succ_iff_of_not_isMax hi).symm)

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