Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 17:49 da6aceb8

View on Github →

chore(order): fix-ups after #9891 (#10538)

Estimated changes

Modified src/combinatorics/simple_graph/subgraph.lean

Modified src/data/fin/basic.lean

Modified src/order/bounded_order.lean

modified theorem inf_eq_bot_iff_le_compl

Modified src/order/filter/germ.lean