Commit 2024-11-04 10:42 51a3c0a3

View on Github →

feat: quotient lift on a finite family (#5576) In the future it may be used to prove that ZFSet is a model of ZF set theory without using Classical.choice. Specifically, it will be used to prove that all first-order formulas of ZFSet are definable. Comparing to (finChoice q).liftOn f, finLiftOn q f asks users to provide a proof of (∀ i, a i ≈ b i) → f a = f b instead of a ≈ b → f a = f b, which is more readable and easier to rewrite. It also makes it easier for users to discover and use relevant APIs.

Estimated changes

Modified Mathlib/Data/Fintype/Quotient.lean

added theorem Quotient.eval_finChoice

modified def Quotient.finChoice

deleted def Quotient.finChoiceAux

deleted theorem Quotient.finChoiceAux_eq

added def Quotient.finChoiceEquiv

modified theorem Quotient.finChoice_eq

added def Quotient.finHRecOn

added theorem Quotient.finHRecOn_mk

added def Quotient.finLiftOn

added theorem Quotient.finLiftOn_empty

added theorem Quotient.finLiftOn_mk

added def Quotient.finRecOn

added theorem Quotient.finRecOn_mk

added theorem Quotient.ind_fintype_pi

added theorem Quotient.induction_on_fintype_pi

added def Quotient.listChoice

added theorem Quotient.listChoice_mk

added theorem Quotient.list_ind

modified def Trunc.finChoice

added def Trunc.finChoiceEquiv

modified theorem Trunc.finChoice_eq

added def Trunc.finLiftOn

added theorem Trunc.finLiftOn_empty

added theorem Trunc.finLiftOn_mk

added def Trunc.finRecOn

added theorem Trunc.finRecOn_mk

Modified Mathlib/Data/Quot.lean

added def Quotient.eval

added theorem Quotient.eval_mk