Theorems · Theorem · order theory

IsSimpleOrder.equivBool_symm_apply

∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : LE α] [inst_2 : BoundedOrder α] [inst_3 : IsSimpleOrder α] (x : Bool),
  IsSimpleOrder.equivBool.symm x = Bool.casesOn x ⊥ ⊤

Defined in: Mathlib.Order.Atoms
Cited by: 0 results in Mathlib
Foundations: Depth 14 from the axioms · uses propext, Quot.sound
Assumes: DecidableEq LE BoundedOrder IsSimpleOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Top.topstatement · cited by 9,680
Equivstatement · cited by 8,337
Bot.botstatement · cited by 4,720
Equiv.symmstatement and proof · cited by 3,681
BoundedOrderstatement and proof · cited by 270
IsSimpleOrderstatement and proof · cited by 54
IsSimpleOrder.equivBoolstatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.