single_of_single_apply — Mathlib

English

The two-sided equation linking nested singles: single a (single a' b) a equals single a' (single a' b) a.

Русский

Связь вложенных одиноких функций: single a (single a' b) a = single a' (single a' b) a.

LaTeX

$$$$\\text{single } a\\, (\\text{single } a'\\, b)\\, a = \\text{single } a'\\, (\\text{single } a'\\, b)\\, a.$$$$

Lean4

theorem single_of_single_apply (a a' : α) (b : M) : single a ((single a' b) a) = single a' (single a' b) a := by
  classical
  rw [single_apply, single_apply]
  ext
  split_ifs with h
  · rw [h]
  · rw [zero_apply, single_apply, ite_self]

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