finChoice_eq — Mathlib

English

Equality of finChoice applied to mk of a is equal to the mk of a in the quotient piSetoid.

Русский

Справедливость для finChoice при mk: равенство между finChoice (⟦a⟧) и ⟦a⟧ в pisetoid-представлении.

LaTeX

$$$\\operatorname{finChoice} (S := S) (\\langle a \\rangle) = \\langle a \\rangle$$$

Lean4

theorem finChoice_eq (a : ∀ i, α i) : finChoice (S := S) (⟦a ·⟧) = ⟦a⟧ :=
  by
  dsimp [finChoice]
  obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep
  simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]
  rfl

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