listChoice_mk — Mathlib

English

For quotients indexed by a list, a canonical equality holds between the list-choice of a representative and the representative itself.

Русский

Для фактор-групп, индексируемых списком, существует каноническое равенство между выбором списка и самим представителем.

LaTeX

$$$\\mathrm{listChoice}(S)\\, (\\llbracket a \\cdot \\cdot \\rrbracket) = \\llbracket a \\rrbracket$$$

Lean4

theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧ :=
  match l with
  | [] => Quotient.sound nofun
  | i :: l => by
    unfold listChoice List.Pi.tail
    rw [listChoice_mk]
    exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

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