Commit 2020-07-28 22:08 2e6c488c
View on Github →chore(order/complete_lattice): use Prop args in infi_inf etc (#3611)
This way one can rw binfi_inf first, then prove ∃ i, p i.
Also move some code up to make it available near infi_inf.
chore(order/complete_lattice): use Prop args in infi_inf etc (#3611)
This way one can rw binfi_inf first, then prove ∃ i, p i.
Also move some code up to make it available near infi_inf.