Commit 2022-12-13 10:52 e6cc6895

View on Github →

feat port: Order.Directed (#963) cf9386b56953fb40904843af98b7a80757bbe7f9 A few name changes in other files

Estimated changes

added theorem Antitone.directed_ge
added theorem Antitone.directed_le
added theorem Directed.extend_bot
added theorem Directed.mono
added theorem Directed.mono_comp
added def Directed
added theorem DirectedOn.mono'
added theorem DirectedOn.mono
added def DirectedOn
added theorem Monotone.directed_ge
added theorem Monotone.directed_le
added theorem directedOn_of_sup_mem
added theorem directedOn_univ
added theorem directedOn_univ_iff
added theorem directed_comp
added theorem directed_id
added theorem directed_id_iff
added theorem directed_of
added theorem directed_of_inf
added theorem directed_of_sup
added theorem directed_on_image
added theorem directed_on_of_inf_mem
added theorem exists_ge_ge
added theorem exists_le_le
added theorem isBot_iff_is_min
added theorem isBot_or_exists_lt
added theorem isTop_iff_is_max
added theorem isTop_or_exists_gt
added theorem is_directed_mono