le_piecewise — Mathlib

English

If g ≤ f1 on s and g ≤ f2 on sᶜ, then g ≤ s.piecewise f1 f2.

Русский

Если g ≤ f1 на s и g ≤ f2 на дополнении s, тогда g ≤ s.piecewise f1 f2.

LaTeX

$$$\\bigl(\\forall i\\in s, g(i) \\le f_1(i)\\bigr) \\land \\bigl(\\forall i\\notin s, g(i) \\le f_2(i)\\bigr) \\Rightarrow \\forall i,\\ g(i) \\le (s.\\mathrm{piecewise} f_1 f_2)(i)$$$

Lean4

theorem le_piecewise {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g : ∀ i, δ i}
    (h₁ : ∀ i ∈ s, g i ≤ f₁ i) (h₂ : ∀ i ∉ s, g i ≤ f₂ i) : g ≤ s.piecewise f₁ f₂ :=
  @piecewise_le α (fun i => (δ i)ᵒᵈ) _ s _ _ _ _ h₁ h₂

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