English
If for all s we have m1(s) = op(m2(s), m3(s)), then for all s we have m1.trim(s) = op(m2.trim(s), m3.trim(s)).
Русский
Если для всех множества s выполнено m1(s) = op(m2(s), m3(s)), то для всех 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) (m₃ s)` for all `s`, then the same is true for `m₁.trim`, `m₂.trim`,
and `m₃ s`. -/
theorem trim_binop {m₁ m₂ m₃ : OuterMeasure α} {op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞} (h : ∀ s, m₁ s = op (m₂ s) (m₃ s))
(s : Set α) : m₁.trim s = op (m₂.trim s) (m₃.trim s) :=
by
rcases exists_measurable_superset_forall_eq_trim ![m₁, m₂, m₃] s with ⟨t, _hst, _ht, htm⟩
simp only [Fin.forall_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm
rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]
