Utility Lemmas

Small lemmas about Empty.elim, Fin.elim0, Fin.snoc, and Fin.append that are used across the infinitary logic library but not (yet) in Mathlib.

theorem Empty.eq_elim {α : Sort u} (f : Empty → α) : f = elim

Any function from Empty equals Empty.elim.

theorem comp_empty_elim {α : Sort u} {β : Sort v} (f : α → β) : f ∘ Empty.elim = Empty.elim

Any function composed with Empty.elim is Empty.elim.

theorem comp_fin_elim0 {α : Type u} {β : Type v} (f : α → β) : f ∘ Fin.elim0 = Fin.elim0

Any function composed with Fin.elim0 is Fin.elim0.

theorem Fin.eq_elim0 {α : Type u} (f : Fin 0 → α) : f = elim0

Any function from Fin 0 equals Fin.elim0.

theorem Fin.snoc_elim0_eq {α : Type u} (x : α) : snoc elim0 x = fun (x_1 : Fin (0 + 1)) => x

Fin.snoc Fin.elim0 x is the constant function fun _ => x on Fin 1.