Theorems · Theorem · order theory

maximal_iff

∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : PartialOrder α], Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → x = y

Defined in

Mathlib.Order.Minimal

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PartialOrder