mem_of_max — Mathlib

English

If the maximum of s equals a, then a is a member of s.

Русский

Если максимум s равен a, то a принадлежит s.

LaTeX

$$$s_{\max} = a \Rightarrow a \in s$$$

Lean4

theorem mem_of_max {s : Finset α} : ∀ {a : α}, s.max = a → a ∈ s := by
  induction s using Finset.induction_on with
  | empty => intro _ H; cases H
  | insert b s _ ih =>
    intro a h
    by_cases p : b = a
    · induction p
      exact mem_insert_self b s
    · rcases max_choice (↑b) s.max with q | q <;> rw [max_insert, q] at h
      · cases h
        cases p rfl
      · exact mem_insert_of_mem (ih h)

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