Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 00:16 db181446

View on Github →

chore(order/bounded_lattice): add is_compl.inf_left_eq_bot_iff etc (#3460)

Estimated changes

Modified src/order/bounded_lattice.lean

added theorem is_compl.disjoint_left_iff

added theorem is_compl.disjoint_right_iff

added theorem is_compl.inf_left_eq_bot_iff

added theorem is_compl.inf_right_eq_bot_iff

Modified src/topology/basic.lean