succAboveOrderIso — Mathlib

English

For any i ∈ Fin(n+2), there is an order isomorphism between Fin(n+1) and the complement {i}ᶜ ⊆ Fin(n+2) given by a ↦ succAbove i a.

Русский

Для любого i ∈ Fin(n+2) существует порядок-изоморфизм между Fin(n+1) и множеством-остатком {i}ᶜ ⊆ Fin(n+2), заданный отображением a ↦ succAbove i a.

LaTeX

$$$\text{succAboveOrderIso}(i):\; \mathrm{Fin}(n+1) \cong_o \{i\}^{c} \subseteq \mathrm{Fin}(n+2).$$$

Lean4

/-- Given `i : Fin (n + 2)`, this is the order isomorphism
between `Fin (n + 1)` and the finite set `{i}ᶜ`. -/
noncomputable def succAboveOrderIso {n : ℕ} (i : Fin (n + 2)) : Fin (n + 1) ≃o ({ i }ᶜ : Finset (Fin (n + 2)))
    where
  toEquiv :=
    Equiv.ofBijective (f := fun a ↦ ⟨Fin.succAboveOrderEmb i a, by simp⟩)
      (by
        constructor
        · intro a b h
          exact (Fin.succAboveOrderEmb i).injective (by simpa using h)
        · rintro ⟨j, hj⟩
          simp only [mem_compl, mem_singleton] at hj
          obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
          · exact ⟨j.pred hj, by simp⟩
          · exact ⟨i.predAbove j, by aesop⟩)
  map_rel_iff' {a b} := by simp only [Equiv.ofBijective_apply, Subtype.mk_le_mk, OrderEmbedding.le_iff_le]

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