ae_null_of_comp_null — Mathlib

English

If (η ∘ κ) a s = 0, then η(·, s) =ᵐ[κ a] 0.

Русский

Если (η ∘ κ) a s = 0, тогда η(·, s) =ᵐ[κ a] 0.

LaTeX

$$$(\\eta \\circ_k \\kappa)(a,s) = 0 \\Rightarrow (\\eta \\cdot s) =^{\\kappa a} 0.$$$

Lean4

theorem ae_null_of_comp_null (h : (η ∘ₖ κ) a s = 0) : (η · s) =ᵐ[κ a] 0 :=
  by
  obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
  simp_rw [comp_null a mt] at ht
  rw [Filter.eventuallyLE_antisymm_iff]
  exact ⟨Filter.EventuallyLE.trans_eq (ae_of_all _ fun _ ↦ measure_mono hst) ht, ae_of_all _ fun _ ↦ zero_le _⟩

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