Commit 2026-03-23 08:24 c6ec2a4d

View on Github →

chore(Order/Lattice): use to_dual for lemmas about Monotone (#37005)

Estimated changes

deleted theorem Antitone.le_map_inf
deleted theorem Antitone.map_inf
deleted theorem AntitoneOn.map_inf
deleted theorem AntitoneOn.of_map_sup
deleted theorem Monotone.map_inf
deleted theorem Monotone.map_inf_le
deleted theorem Monotone.of_map_inf
deleted theorem Monotone.of_map_inf_le
deleted theorem MonotoneOn.map_inf
deleted theorem MonotoneOn.of_map_inf