English
Given a predicate p on β, and a choice of functions f and g that select values depending on p, the chosen value at b is below the supremum of the entire family when b ∈ s and p(b) holds.
Русский
Для предиката p на β и функций f,g выбирающих значения в зависимости от p, значение в точке b ≤ супремум всей fam (при условии b ∈ s и p(b)).
LaTeX
$$$(h_0 : b \in s) (h_1 : p b) : f b h_1 \le s.sup (\lambda i. indicator{p i} \;f i h_1 \;else\; g i h_1)$$$
Lean4
theorem le_sup_dite_pos (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β}
(h₀ : b ∈ s) (h₁ : p b) : f b h₁ ≤ s.sup fun i ↦ if h : p i then f i h else g i h :=
by
have : f b h₁ = (fun i ↦ if h : p i then f i h else g i h) b := by simp [h₁]
rw [this]
apply le_sup h₀
