English
Let p be a predicate on β with decidable predicate. For any b ∈ s with not p(b), the infimum over i ∈ s of (if p(i) then f(i,h) else g(i,h)) is ≤ g(b,h).
Русский
Пусть p — предикат на β с разрешимым предикатом. Для любого b ∈ s с ¬p(b) справедливо: inf_{i∈s} (if p(i) then f(i,h) else g(i,h)) ≤ g(b,h).
LaTeX
$$$ (b \\in s) \\land \\neg p(b) \\Rightarrow s.\\inf (i \\mapsto if p(i) then f(i,h) else g(i,h)) \\le g(b,h) $$$
Lean4
theorem inf_dite_neg_le (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β}
(h₀ : b ∈ s) (h₁ : ¬p b) : (s.inf fun i ↦ if h : p i then f i h else g i h) ≤ g b h₁ :=
by
have : g b h₁ = (fun i ↦ if h : p i then f i h else g i h) b := by simp [h₁]
rw [this]
apply inf_le h₀
