eval_finChoice

Mathlib.Data.Fintype.Quotient

URI: https://scilib.ai/kg/mathlib#Quotient.eval_finChoice

English

Applying eval to finChoice recovers the original family of quotients.

Русский

Применение операции eval к finChoice восстанавливает исходную семью фактор-объектов.

LaTeX

$$$\\operatorname{eval}(\\operatorname{finChoice} f) = f$$$

Lean4

theorem eval_finChoice (f : ∀ i, Quotient (S i)) : eval (finChoice f) = f :=
  induction_on_fintype_pi f (fun a ↦ by rw [finChoice_eq]; rfl)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru