orderEmbOfFin_zero — Mathlib

English

The image of 0 under the order-embedding of a finite set is the minimum element of that set.

Русский

Изображение нуля под orderEmbOfFin есть минимальный элемент множества.

LaTeX

$$orderEmbOfFin\,s\,h\,0 = s.min'\,(card_pos.mp (h.symm \rarr hz))$$

Lean4

/-- The bijection `orderEmbOfFin s h` sends `0` to the minimum of `s`. -/
theorem orderEmbOfFin_zero {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
    orderEmbOfFin s h ⟨0, hz⟩ = s.min' (card_pos.mp (h.symm ▸ hz)) := by
  simp only [orderEmbOfFin_apply, Fin.getElem_fin, sorted_zero_eq_min']

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