comapDomain_zero — Mathlib

English

If h is injective and each β i has a zero element, then comapDomain h hh maps zero to zero.

Русский

Пусть h: κ → ι инъективно и ∀ i имеется 0 в β i; тогда comapDomain h hh отображает ноль в ноль.

LaTeX

$$$\\mathrm{comapDomain}(h, hh)(0) = 0$$$

Lean4

@[simp]
theorem comapDomain_zero [∀ i, Zero (β i)] (h : κ → ι) (hh : Function.Injective h) :
    comapDomain h hh (0 : Π₀ i, β i) = 0 := by
  ext
  rw [zero_apply, comapDomain_apply, zero_apply]

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