max_erase_ne_self — Mathlib

English

For any x and finite set s, removing x yields (s.erase x).max ≠ x.

Русский

Для любого x и конечного множества s, удаление x приводит к тому, что максимальный элемент множества без x не равен x.

LaTeX

$$$ (s.erase x).max \\neq x $$$

Lean4

theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x :=
  by
  by_cases s0 : (s.erase x).Nonempty
  · refine ne_of_eq_of_ne (coe_max' s0).symm ?_
    exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
  · rw [not_nonempty_iff_eq_empty.mp s0, max_empty]
    exact WithBot.bot_ne_coe

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