instNeZeroMeasureCoeSectLOfProdMk

English

Let κ be a kernel from α × β to γ. If κ(a, b) is nonzero for some a ∈ α and b ∈ β, then the left section of κ at b, evaluated at a, is also nonzero; i.e. (sectL κ b)(a) ≠ 0.

Русский

Пусть κ—ядро из α × β в γ. Если κ(a, b) ненулевое для некоторого a ∈ α и b ∈ β, то левый срез κ в точке b, применённый к a, также ненулевой; то есть (sectL κ b)(a) ≠ 0.

LaTeX

$$$\kappa(a,b) \ne 0 \Rightarrow (\sectL \kappa b)(a) \ne 0$$$

Lean4

instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectL κ b) a) := by rw [sectL_apply];
  infer_instance

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