The kernel_hom tactic transforms a kernel equality to an equivalent equality in the category of measurable spaces and s-finite kernels.

The tactic supports location specifiers like rw or simp:

• kernel_hom — applies to the goal

• kernel_hom at h — applies to hypothesis h

• kernel_hom at h₁ h₂ — applies to multiple hypotheses

• kernel_hom at h ⊢ — applies to hypothesis h and the goal

• kernel_hom at * — applies to all hypotheses and the goal

Example:

example {W X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
    [MeasurableSpace W] (κ : Kernel X Y) (η : Kernel Y Z) (ξ : Kernel Z W)
    [IsFiniteKernel ξ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    ξ ∘ₖ (η ∘ₖ κ) = ξ ∘ₖ η ∘ₖ κ := by
  kernel_hom
  exact Category.assoc _ _ _

kernelHom : Lean.ParserDescr
kernelHom : Lean.ParserDescr

Code

Actions: Source · Open Issue