orderEmbOfFin_last — Mathlib

English

The image of k-1 under the order-embedding is the maximum element of the set.

Русский

Изображение k-1 под orderEmbOfFin есть максимум множества.

LaTeX

$$orderEmbOfFin\,s\,h\,⟨k-1, \_⟩ = s.max'\,(card_pos.mp (h.symm \rarr hz))$$

Lean4

/-- The bijection `orderEmbOfFin s h` sends `k-1` to the maximum of `s`. -/
theorem orderEmbOfFin_last {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
    orderEmbOfFin s h ⟨k - 1, Nat.sub_lt hz (Nat.succ_pos 0)⟩ = s.max' (card_pos.mp (h.symm ▸ hz)) := by
  simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]

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