isSFiniteKernel_prodMkRight_unit — Mathlib

English

IsSFiniteKernel (prodMkRight Unit κ) holds iff IsSFiniteKernel κ holds.

Русский

IsSFiniteKernel (prodMkRight Unit κ) выполняется тогда и только тогда, когда IsSFiniteKernel κ выполняется.

LaTeX

$$$\operatorname{IsSFiniteKernel}(\operatorname{prodMkRight} Unit \kappa) \;\Leftrightarrow\; \operatorname{IsSFiniteKernel}(\kappa)$$$

Lean4

theorem isSFiniteKernel_prodMkRight_unit {κ : Kernel α β} : IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ :=
  by
  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  change IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a ↦ (a, ())) (by fun_prop))
  infer_instance

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