map — Mathlib

English

If κ is finite, then map κ f is finite.

Русский

Если κ конечное ядро, то map κ f конечное.

LaTeX

$$$$ \\text{IsFiniteKernel}(\\kappa) \\implies \\text{IsFiniteKernel}(\\kappa.map f). $$$$

Lean4

instance map (κ : Kernel α β) [IsFiniteKernel κ] (f : β → γ) : IsFiniteKernel (map κ f) :=
  by
  refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
  by_cases hf : Measurable f
  · rw [map_apply' κ hf a MeasurableSet.univ]
    exact measure_le_bound κ a _
  · simp [map_of_not_measurable _ hf]

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