comapDomain_single — Mathlib

English

comapDomain h hh (single (h k) x) = single k x.

Русский

comapDomain h hh (single (h k) x) = single k x.

LaTeX

$$$\\mathrm{comapDomain}(h, hh)(\\mathrm{single}(h k) x) = \\mathrm{single}(k) x$$$

Lean4

@[simp]
theorem comapDomain_single [DecidableEq ι] [DecidableEq κ] [∀ i, Zero (β i)] (h : κ → ι) (hh : Function.Injective h)
    (k : κ) (x : β (h k)) : comapDomain h hh (single (h k) x) = single k x :=
  by
  ext i
  rw [comapDomain_apply]
  obtain rfl | hik := Decidable.eq_or_ne i k
  · rw [single_eq_same, single_eq_same]
  · rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]

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