mono — Mathlib

English

If h is HasIntegral with a finer parameter l1 and l2 ≤ l1, then h also holds for l2 (HasIntegral is monotone in l).

Русский

Если HasIntegral выполнено для более точного параметра l1, и l2 ≤ l1, то HasIntegral выполняется и для l2.

LaTeX

$$$\text{HasIntegral}(I, l_1, f, vol, y) \to \text{HasIntegral}(I, l_2, f, vol, y) \quad \text{whenever } l_2 \le l_1$$$

Lean4

theorem mono {l₁ l₂ : IntegrationParams} (h : HasIntegral I l₁ f vol y) (hl : l₂ ≤ l₁) : HasIntegral I l₂ f vol y :=
  h.mono_left <| IntegrationParams.toFilteriUnion_mono _ hl _

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