Commit 2022-12-30 17:08 8618f40d

View on Github →

feat: port Order.Atoms (#1257)

depends on: #1258

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Atoms.lean

added theorem GaloisCoinsertion.isAtom_iff

added theorem GaloisCoinsertion.isAtom_of_image

added theorem GaloisCoinsertion.isCoatom_iff'

added theorem GaloisCoinsertion.isCoatom_iff

added theorem GaloisCoinsertion.isCoatom_of_l_top

added theorem GaloisInsertion.isAtom_iff'

added theorem GaloisInsertion.isAtom_iff

added theorem GaloisInsertion.isAtom_of_u_bot

added theorem GaloisInsertion.isCoatom_iff

added theorem GaloisInsertion.isCoatom_of_image

added theorem IsAtom.Iic

added theorem IsAtom.Iic_eq

added theorem IsAtom.disjoint_of_ne

added theorem IsAtom.inf_eq_bot_of_ne

added theorem IsAtom.le_iff

added theorem IsAtom.lt_iff

added theorem IsAtom.of_isAtom_coe_Iic

added def IsAtom

added theorem IsCoatom.Ici

added theorem IsCoatom.Ici_eq

added theorem IsCoatom.le_iff

added theorem IsCoatom.lt_iff

added theorem IsCoatom.of_isCoatom_coe_Ici

added theorem IsCoatom.sup_eq_top_of_ne

added def IsCoatom

added theorem IsCompl.isAtom_iff_isCoatom

added theorem IsCompl.isCoatom_iff_isAtom

added theorem IsSimpleOrder.bot_ne_top

added theorem IsSimpleOrder.eq_bot_of_lt

added theorem IsSimpleOrder.eq_top_of_lt

added def IsSimpleOrder.equivBool

added def IsSimpleOrder.orderIsoBool

added theorem OrderEmbedding.isAtom_of_map_bot_of_image

added theorem OrderEmbedding.isCoatom_of_map_top_of_image

added theorem OrderIso.isAtom_iff

added theorem OrderIso.isCoatom_iff

added theorem OrderIso.isSimpleOrder

added theorem OrderIso.isSimpleOrder_iff

added theorem Set.Ici.isAtom_iff

added theorem Set.Iic.isCoatom_iff

added theorem Set.isAtom_iff

added theorem Set.isAtom_singleton

added theorem Set.isCoatom_iff

added theorem Set.isCoatom_singleton_compl

added theorem Set.isSimpleOrder_Ici_iff_isCoatom

added theorem Set.isSimpleOrder_Iic_iff_isAtom

added theorem bot_covby_iff

added theorem bot_covby_top

added theorem covby_iff_atom_Ici

added theorem covby_iff_coatom_Iic

added theorem covby_top_iff

added theorem isAtom_dual_iff_isCoatom

added theorem isAtom_iff

added theorem isAtom_top

added theorem isAtomic_dual_iff_isCoatomic

added theorem isAtomic_iff_forall_isAtomic_Iic

added theorem isAtomic_iff_isCoatomic

added theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular

added theorem isAtomic_of_orderBot_wellFounded_lt

added theorem isAtomistic_dual_iff_isCoatomistic

added theorem isCoatom_bot

added theorem isCoatom_dual_iff_isAtom

added theorem isCoatom_iff

added theorem isCoatomic_dual_iff_isAtomic

added theorem isCoatomic_iff_forall_isCoatomic_Ici

added theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

added theorem isCoatomic_of_orderTop_gt_wellFounded

added theorem isCoatomistic_dual_iff_isAtomistic

added theorem isSimpleOrder_iff_isAtom_top

added theorem isSimpleOrder_iff_isCoatom_bot

added theorem isSimpleOrder_iff_isSimpleOrder_orderDual

added theorem le_iff_atom_le_imp

added theorem supₛ_atoms_eq_top

added theorem supₛ_atoms_le_eq