max'_erase_ne_self — Mathlib

English

If, after removing a element x from s, the remaining set is nonempty, then the maximum of the erased set is not equal to x.

Русский

Если после удаления элемента x из s получившееся множество непустое, то максимальное элемента s, оставшегося после удаления, не равно x.

LaTeX

$$$ (s\\setminus \\{x\\}).max' {s \\setminus x}.Nonempty \\, \\Rightarrow \\, (s\\setminus x).max' \\neq x $$$

Lean4

theorem max'_erase_ne_self {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).max' s0 ≠ x :=
  ne_of_mem_erase (max'_mem _ s0)

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