Theorem Subtype.mk_inf_mk

Modification history

2025-12-24 12:03

Mathlib/Order/Lattice.lean

feat(Order/Lattice): use `@[to_dual]` (#33142) …

Deleted Subtype.mk_inf_mk View on Github →

2022-11-25 17:46

Mathlib/Order/Lattice.lean

feat: port Order.Lattice (#642) …

Added Subtype.mk_inf_mk View on Github →