Theorem CompleteLatticeHom.coe_tosSupHom

Modification history

2026-03-26 22:21

Mathlib/Order/Hom/CompleteLattice.lean

chore(Order/Hom/CompleteLattice): use `to_dual` (#37035) …

Deleted CompleteLatticeHom.coe_tosSupHom View on Github →

2023-10-20 09:11

Mathlib/Order/Hom/CompleteLattice.lean

fix(Order/Hom): coercion lemmas for lattice and complete lattice (#7796) …

Added CompleteLatticeHom.coe_tosSupHom View on Github →