Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 21:44 3ac971be

View on Github →

feat(order/category/Frame): The category of frames (#12363) Define Frame, the category of frames with frame homomorphisms.

Estimated changes

added def Frame.hom
added def Frame.iso.mk
added def Frame.of
added def Frame