finset_sup_eq — Mathlib

English

If a is SupIrred and s.sup f = a, then there exists i ∈ s with f i = a.

Русский

Если a — SupIrred и s.sup f = a, то существует i ∈ s такое, что f i = a.

LaTeX

$$SupIrred\ a \rightarrow s.sup f = a \rightarrow \exists i \in s, f i = a$$

Lean4

theorem finset_sup_eq (ha : SupIrred a) (h : s.sup f = a) : ∃ i ∈ s, f i = a := by
  classical
    induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih

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