Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-04 18:23 05e2fc02

View on Github →

chore(order/*): generalisation linter (#13105)

Estimated changes

Modified src/order/atoms.lean

modified theorem set.is_simple_order_Ici_iff_is_coatom

modified theorem set.is_simple_order_Iic_iff_is_atom

Modified src/order/conditionally_complete_lattice.lean

Modified src/order/lattice_intervals.lean

modified theorem set.Ici.coe_bot

modified theorem set.Iic.coe_top

Modified src/order/modular_lattice.lean

Modified src/order/order_iso_nat.lean