English
Assume a > ⊥. Then a ≤ sup f iff there exists some b ∈ s with a ≤ f(b).
Русский
Пусть a > ⊥. Тогда a ≤ sup f ⇔ существует b ∈ s такое, что a ≤ f(b).
LaTeX
$$$a > \bot \Rightarrow (a \le s \sup f \iff \exists b \in s, a \le f(b))$$$
Lean4
@[simp]
protected theorem le_sup_iff (ha : ⊥ < a) : a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b :=
by
apply Iff.intro
·
induction s using cons_induction with
| empty => exact (absurd · (not_le_of_gt ha))
| cons c t hc ih =>
rw [sup_cons, le_sup_iff]
exact fun
| Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
| Or.inr h =>
let ⟨b, hb, hle⟩ := ih h;
⟨b, mem_cons.2 (Or.inr hb), hle⟩
· exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)
