trim_op — Mathlib

English

If m1(s) = op(m2(s), m3(s)) for all s, then m1.trim(s) = op(m2.trim(s), m3.trim(s).

Русский

Если для всех s выполняется m1(s) = op(m2(s), m3(s)), то m1.trim(s) = op(m2.trim(s), m3.trim(s)).

LaTeX

$$$$ \forall s,\; m_1(s) = \operatorname{op}(m_2(s), m_3(s)) \Rightarrow m_1^{\mathrm{trim}}(s) = \operatorname{op}(m_2^{\mathrm{trim}}(s), m_3^{\mathrm{trim}}(s)). $$$$

Lean4

/-- If `m₁ s = op (m₂ s)` for all `s`, then the same is true for `m₁.trim` and `m₂.trim`. -/
theorem trim_op {m₁ m₂ : OuterMeasure α} {op : ℝ≥0∞ → ℝ≥0∞} (h : ∀ s, m₁ s = op (m₂ s)) (s : Set α) :
    m₁.trim s = op (m₂.trim s) :=
  @trim_binop α _ m₁ m₂ 0 (fun a _b => op a) h s

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