ae_lt_top_of_comp_ne_top — Mathlib

English

Kernel composition is associative: (ξ ∘ η) ∘ κ = ξ ∘ (η ∘ κ).

Русский

Компоновка ядер ассоциативна: (ξ ∘ η) ∘ κ = ξ ∘ (η ∘ κ).

LaTeX

$$$(\\xi \\circ \\eta) \\circ \\kappa = \\xi \\circ (\\eta \\circ \\kappa).$$$

Lean4

theorem ae_lt_top_of_comp_ne_top (a : α) (hs : (η ∘ₖ κ) a s ≠ ∞) : ∀ᵐ b ∂κ a, η b s < ∞ :=
  by
  have h : ∀ᵐ b ∂κ a, η b (toMeasurable ((η ∘ₖ κ) a) s) < ∞ :=
    by
    refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_
    rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]
  filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb

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