Mathlib Map

Theorems · Theorem · order theory

IsGreatest.maximal

∀ {α : Type u_2} {x : α} {s : Set α} [inst : Preorder α], IsGreatest s x → Maximal (fun x => x ∈ s) x
Defined in
Mathlib.Order.Minimal
Cited by
1 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsGreatest.maximal_iff · cited by 1IsGreatest.maximal_iffSet · cited by 53352SetPreorder · cited by 7952PreorderMaximal · cited by 211MaximalIsGreatest · cited by 112IsGreatestIsGreatest.maximalCITED BYCITES

Cites4

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

  • Setstatement and proof · cited by 53,352
  • Preorderstatement and proof · cited by 7,952
  • Maximalstatement · cited by 211
  • IsGreateststatement and proof · cited by 112

Cited by1

Results whose statement or proof uses this declaration.