Mathlib Map

Theorems · Definition · order theory

IsAtomic.casesOn

{α : Type u_2} →
  [inst : PartialOrder α] →
    [inst_1 : OrderBot α] →
      {motive : IsAtomic α → Sort u} →
        (t : IsAtomic α) → ((eq_bot_or_exists_atom_le : ∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b) → motive ⋯) → motive t
Defined in
Mathlib.Order.Atoms
Cited by
1 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
PartialOrderOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isAtomic_iff · cited by 0isAtomic_iffPartialOrder · cited by 6410PartialOrderBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotIsAtom · cited by 130IsAtomIsAtomic · cited by 20IsAtomicIsAtomic.casesOnCITED BYCITES

Cites5

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

  • PartialOrderstatement and proof · cited by 6,410
  • Bot.botstatement and proof · cited by 4,720
  • OrderBotstatement and proof · cited by 1,055
  • IsAtomstatement and proof · cited by 130
  • IsAtomicstatement and proof · cited by 20

Cited by1

Results whose statement or proof uses this declaration.