le_add_caratheodory — Mathlib

English

The meet of Carathéodorys of m1 and m2 is bounded by the Carathéodory of m1 + m2.

Русский

Наименьшее из Caratheodory(m1) и Caratheodory(m2) не превосходит Caratheodory(m1 + m2).

LaTeX

$$m1.caratheodory ⊓ m2.caratheodory ≤ (m1 + m2).caratheodory$$

Lean4

theorem le_add_caratheodory (m₁ m₂ : OuterMeasure α) :
    m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂ : OuterMeasure α).caratheodory := fun s ⟨hs₁, hs₂⟩ t => by
  simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]

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