isSFiniteKernel_prodMkRight_iff — Mathlib

English

For [Nonempty γ], IsSFiniteKernel (prodMkRight γ κ) holds iff IsSFiniteKernel κ.

Русский

Для непустого γ: IsSFiniteKernel (prodMkRight γ κ) эквивалентно IsSFiniteKernel κ.

LaTeX

$$IsSFiniteKernel (prodMkRight γ κ) ↔ IsSFiniteKernel κ$$

Lean4

theorem isSFiniteKernel_prodMkRight_iff [Nonempty γ] {κ : Kernel α β} :
    IsSFiniteKernel (prodMkRight γ κ) ↔ IsSFiniteKernel κ :=
  by
  inhabit γ
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← sectL_prodMkRight γ κ default]
  infer_instance

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