isFiniteKernel_of_isFiniteKernel_fst

English

If κ is IsSFiniteKernel, then fst κ is IsSFiniteKernel.

Русский

Если κ IsSFiniteKernel, то fst κ IsSFiniteKernel.

LaTeX

$$$$\\text{IsSFiniteKernel}(\\kappa) \\Rightarrow \\text{IsSFiniteKernel}(\\mathrm{fst}\\,\\kappa)$$$$

Lean4

instance (priority := 100) isFiniteKernel_of_isFiniteKernel_fst {κ : Kernel α (β × γ)} [h : IsFiniteKernel (fst κ)] :
    IsFiniteKernel κ :=
  by
  refine ⟨(fst κ).bound, (fst κ).bound_lt_top, fun a ↦ le_trans ?_ (measure_le_bound (fst κ) a Set.univ)⟩
  rw [fst_apply' _ _ MeasurableSet.univ]
  simp

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