elim_swap — Mathlib

English

For functions f,g: α → γ, β → γ, the composition (Sum.elim f g) ∘ Sum.swap equals Sum.elim g f as functions α ⊕ β → γ.

Русский

Для функций f,g: α → γ, β → γ выполнено равенство (Sum.elim f g) ∘ Sum.swap = Sum.elim g f как функции α ⊕ β → γ.

LaTeX

$$$(\mathrm{Sum.elim} f g) \circ \mathrm{Sum.swap} = \mathrm{Sum.elim} g f$$$

Lean4

@[simp]
theorem elim_swap {α β γ : Type*} {f : α → γ} {g : β → γ} : Sum.elim f g ∘ Sum.swap = Sum.elim g f :=
  by
  ext x
  cases x with
  | inl x => simp
  | inr x =>
    simp
      -- Lean has removed the `@[simp]` attribute on these. For now Mathlib adds it back.

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