sumProdDistrib_apply_left — Mathlib

English

In the forward direction of the distributive equivalence, the image of (inl a, c) is inl (a, c).

Русский

В направлении отображения по правилу образования левой части эквивалентности: образ (inl a, c) равен inl (a, c).

LaTeX

$$$\text{sumProdDistrib}_{\alpha\beta\gamma}(\text{Sum.inl } a, c) = \text{Sum.inl } (a, c).$$$

Lean4

@[simp]
theorem sumProdDistrib_apply_left {α β γ} (a : α) (c : γ) : sumProdDistrib α β γ (Sum.inl a, c) = Sum.inl (a, c) :=
  rfl

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