Mathlib Map

Theorems · Theorem · order theory

bot_covBy_iff

∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ⋖ a ↔ IsAtom a
Defined in
Mathlib.Order.Atoms
Cited by
4 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PartialOrderOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

covBy_top_iff · cited by 4covBy_top_iffIsAtom.bot_covBy · cited by 3IsAtom.bot_covByCovBy.is_atom · cited by 0CovBy.is_atomSet.Ici.isAtom_iff · cited by 0Ici.isAtom_iffPartialOrder · cited by 6410PartialOrderBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotCovBy · cited by 290CovByIsAtom · cited by 130IsAtombot_covBy_iffCITED 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
  • CovBystatement · cited by 290
  • IsAtomstatement · cited by 130

Cited by4

Results whose statement or proof uses this declaration.