Structures · Order
IsSimpleOrder
An order is simple iff it has exactly two elements, ⊥ and ⊤.
- Defined in
- Mathlib.Order.Atoms
- Shape
- One type argument · adds eq_bot_or_eq_top
Extends1
Extended by1
Concrete types that are instances9
- Bool
- TopologicalSpace.Opens
- AddSubgroup
- TwoSidedIdeal
- AffineSubspace
- CategoryTheory.Subobject
- OrderDual
- Ideal
- Subgroup
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- IsSimpleOrder.eq_bot_or_eq_top
- isAtom_top
- IsSimpleOrder.equivBool
- isAtom_iff_eq_top
- IsSimpleOrder.eq_top_of_lt
- OrderIso.isSimpleOrder
- IsSimpleOrder.eq_bot_of_lt
- isCoatom_bot
- CategoryTheory.simple_of_isSimpleOrder_subobject
- IsSimpleOrder.bot_ne_top
- IsSimpleOrder.bot_lt_iff_eq_top
- IsSimpleOrder.instFintypeOfDecidableEq
- IsSimpleOrder.instIsAtomic
- Order.krullDim_of_isSimpleOrder
- IsSimpleOrder.instIsAtomistic
- OrderDual.instIsSimpleOrder
- IsSimpleOrder.booleanAlgebra
- isCoatom_iff_eq_bot
- IsSimpleOrder.distribLattice
- IsSimpleOrder.toNontrivial
- IsSimpleOrder.equivBool.congr_simp
- IsSimpleOrder.equivBool_apply
- bot_covBy_top
- IsSimpleOrder.orderIsoBool
- IsSimpleOrder.instComplementedLattice
- IsSimpleOrder.equivBool_symm_apply
- IsSimpleOrder.linearOrder
- IsSimpleOrder.lattice
- IsSimpleOrder.completeLattice
- LT.lt.eq_top
- IsSimpleOrder.completeBooleanAlgebra
- Fintype.IsSimpleOrder.univ
- Fintype.IsSimpleOrder.card
- IsSimpleOrder.instIsCoatomic
- IsSimpleOrder.instIsCoatomistic
- IsSimpleOrder.preorder
- IsSimpleOrder.lt_top_iff_eq_bot
- IsSimpleOrder.instFinite
- LT.lt.eq_bot