Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-16 19:01 bf2428c9

View on Github →

feat(order/irreducible): Sup-irreducible elements (#18999) Define sup- and inf- irreducible and prime elements in a lattice.

Estimated changes

added theorem inf_irred.ne_top
added def inf_irred
added theorem inf_irred_of_dual
added theorem inf_irred_to_dual
added theorem inf_prime.inf_le
added theorem inf_prime.ne_top
added def inf_prime
added theorem inf_prime_of_dual
added theorem inf_prime_to_dual
added theorem is_max.not_inf_irred
added theorem is_max.not_inf_prime
added theorem is_min.not_sup_irred
added theorem is_min.not_sup_prime
added theorem not_inf_irred
added theorem not_inf_irred_top
added theorem not_inf_prime
added theorem not_inf_prime_top
added theorem not_sup_irred
added theorem not_sup_irred_bot
added theorem not_sup_prime
added theorem not_sup_prime_bot
added theorem sup_irred.ne_bot
added theorem sup_irred.not_is_min
added def sup_irred
added theorem sup_irred_of_dual
added theorem sup_irred_to_dual
added theorem sup_prime.le_sup
added theorem sup_prime.ne_bot
added theorem sup_prime.not_is_min
added def sup_prime
added theorem sup_prime_of_dual
added theorem sup_prime_to_dual