add_left_iff — Mathlib

English

μ1 + μ2 ≪ ν iff μ1 ≪ ν and μ2 ≪ ν.

Русский

μ1 + μ2 ≪ ν тогда и только тогда, когда μ1 ≪ ν и μ2 ≪ ν.

LaTeX

$$$(\mu_1 + \mu_2) \ll \nu \iff (\mu_1 \ll \nu) \land (\mu_2 \ll \nu)$$$

Lean4

theorem add_left_iff {μ₁ μ₂ ν : Measure α} : μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
  · have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0
    exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩
  · rw [← two_smul ℝ≥0]
    exact AbsolutelyContinuous.rfl.smul_left 2

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