star_sumElim — Mathlib

English

If x:I→α and y:J→α with α a Star-type, then star distributes over Sum.elim: star (Sum.elim x y) = Sum.elim (star x) (star y).

Русский

Если x: I→α и y: J→α и α имеет операцию звезды, то звезда распределяется над Sum.elim: star(Sum.elim x y) = Sum.elim (star x) (star y).

LaTeX

$$$\\star\\big(\\mathrm{Sum.elim}\\ x\\ y\\big) = \\mathrm{Sum.elim}\\ (\\star x)\ (\\star y).$$$

Lean4

theorem star_sumElim {I J α : Type*} (x : I → α) (y : J → α) [Star α] :
    star (Sum.elim x y) = Sum.elim (star x) (star y) := by ext x;
  cases x <;> simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]

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