Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-17 04:51 2bdadb4f

View on Github →

feat(order/imp): define lattice.imp and lattice.biimp (#10327)

Estimated changes

modified theorem sdiff_eq_bot_iff
added def lattice.biimp
added theorem lattice.biimp_comm
added theorem lattice.biimp_eq_iff
added theorem lattice.biimp_mp
added theorem lattice.biimp_mpr
added theorem lattice.biimp_self
added theorem lattice.biimp_symm
added theorem lattice.bot_imp
added theorem lattice.compl_biimp
added theorem lattice.compl_imp
added theorem lattice.compl_sdiff
added def lattice.imp
added theorem lattice.imp_bot
added theorem lattice.imp_eq_arrow
added theorem lattice.imp_eq_bot_iff
added theorem lattice.imp_eq_top_iff
added theorem lattice.imp_inf_le
added theorem lattice.imp_mono
added theorem lattice.imp_self
added theorem lattice.imp_top
added theorem lattice.inf_imp_eq
added theorem lattice.le_imp_iff
added theorem lattice.top_imp