Comment Comment by sanxiyn Lean's three standard axioms are documented in The Lean Language Reference.https://lean-lang.org/doc/reference/latest/Axioms/#standard-...The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → αThe axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = bThe quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b) parent sanxiyn 1 month ago
https://lean-lang.org/doc/reference/latest/Axioms/#standard-...
The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α
The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b
The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)