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 : κ → ι) {h' : ι → κ}
    (hh' : Function.LeftInverse h' 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'.injective.ne hik)]

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