le_finset_sup — Mathlib

English

For any SupPrime a, a ≤ s.sup f iff there exists i ∈ s with a ≤ f i.

Русский

Для любого SupPrime a, a ≤ s.sup f тогда и только тогда, когда существует i ∈ s с a ≤ f i.

LaTeX

$$SupPrime\ a \rightarrow (a \le s.sup f) \leftrightarrow (\exists i \in s, a \le f i)$$

Lean4

theorem le_finset_sup (ha : SupPrime a) : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i := by
  classical
    induction s using Finset.induction with
  | empty => simp [ha.ne_bot]
  | insert i s _ ih => simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]

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