min — Mathlib

English

If l1 ≤ l2 and l2.RCond r holds, then l1.RCond r holds as well.

Русский

Если l1 ≤ l2 и l2.RCond r, то и l1.RCond r выполняется.

LaTeX

$$$l_1 \\le l_2 \\quad \\Rightarrow \\quad l_2.RCond r \\Rightarrow l_1.RCond r$$$

Lean4

nonrec theorem min {ι : Type*} {r₁ r₂ : (ι → ℝ) → Ioi (0 : ℝ)} (h₁ : l.RCond r₁) (h₂ : l.RCond r₂) :
    l.RCond fun x => min (r₁ x) (r₂ x) := fun hR x => congr_arg₂ min (h₁ hR x) (h₂ hR x)

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