Commit 2023-09-17 16:14 9ebe3593

View on Github →

feat: add lemma Quotient.exists (#7220) Also forall_quotient_iff {α : Type*} [r : Setoid α] ... -> Quotient.forall {α : Sort*} {s : Setoid α} ...

Estimated changes

Modified Mathlib/Data/Quot.lean

added theorem Quotient.exists

added theorem Quotient.forall

deleted theorem forall_quotient_iff

Modified Mathlib/ModelTheory/Fraisse.lean

Modified Mathlib/ModelTheory/Ultraproducts.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean