English
If m(u) = ∞ for every u that intersects both s and t nontrivially, then μ(s ∪ t) = μ(s) + μ(t) for μ = ofFunction m m_empty.
Русский
Если для всех u с ненулевым пересечением с s и t выполняется m(u) = ∞, тогда μ(s ∪ t) = μ(s) + μ(t) для μ = ofFunction m m_empty.
LaTeX
$$$\\forall s,t,\\; (∀ u, (s\\cap u).Nonempty ∧ (t\\cap u).Nonempty → m u = ∞) \\\\Rightarrow OuterMeasure.ofFunction m m_empty (s \\cup t) = OuterMeasure.ofFunction m m_empty s + OuterMeasure.ofFunction m m_empty t$$$
Lean4
/-- Given any function `m` assigning measures to sets satisfying `m ∅ = 0`, there is
a unique maximal outer measure `μ` satisfying `μ s ≤ m s` for all `s : Set α`. -/
protected def ofFunction (m : Set α → ℝ≥0∞) (m_empty : m ∅ = 0) : OuterMeasure α :=
let μ s := ⨅ (f : ℕ → Set α) (_ : s ⊆ ⋃ i, f i), ∑' i, m (f i)
{ measureOf := μ
empty := le_antisymm ((iInf_le_of_le fun _ => ∅) <| iInf_le_of_le (empty_subset _) <| by simp [m_empty]) (zero_le _)
mono := fun {_ _} hs => iInf_mono fun _ => iInf_mono' fun hb => ⟨hs.trans hb, le_rfl⟩
iUnion_nat := fun s _ =>
ENNReal.le_of_forall_pos_le_add <| by
intro ε hε (hb : (∑' i, μ (s i)) < ∞)
rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 hε).ne' ℕ with ⟨ε', hε', hl⟩
grw [← hl]
rw [← ENNReal.tsum_add]
choose f hf using
show ∀ i, ∃ f : ℕ → Set α, (s i ⊆ ⋃ i, f i) ∧ (∑' i, m (f i)) < μ (s i) + ε' i
by
intro i
have : μ (s i) < μ (s i) + ε' i :=
ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _) (by simpa using (hε' i).ne')
rcases iInf_lt_iff.mp this with ⟨t, ht⟩
exists t
contrapose! ht
exact le_iInf ht
refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)
rw [← ENNReal.tsum_prod, ← Nat.pairEquiv.symm.tsum_eq]
refine iInf_le_of_le _ (iInf_le _ ?_)
apply iUnion_subset
intro i
apply Subset.trans (hf i).1
apply iUnion_subset
simp only [Nat.pairEquiv_symm_apply]
rw [iUnion_unpair]
intro j
apply subset_iUnion₂ i }
