piecewise_le — Mathlib

English

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

Русский

Если на части s и его дополнения соответствующие неравенства выполняются, то s.piecewise f1 f2 ≤ g.

LaTeX

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

Lean4

theorem piecewise_le {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g : ∀ i, δ i}
    (h₁ : ∀ i ∈ s, f₁ i ≤ g i) (h₂ : ∀ i ∉ s, f₂ i ≤ g i) : s.piecewise f₁ f₂ ≤ g := fun i =>
  if h : i ∈ s then by simp [*] else by simp [*]

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