isSFiniteKernel_prodMkLeft_iff — Mathlib

English

For [Nonempty γ], IsSFiniteKernel (prodMkLeft γ κ) holds if and only if IsSFiniteKernel κ.

Русский

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

LaTeX

$$IsSFiniteKernel (prodMkLeft γ κ) ↔ IsSFiniteKernel κ$$

Lean4

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

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