Theorems · Theorem · order theory

IsGreatest.maximal_iff

∀ {α : Type u_2} {a x : α} {s : Set α} [inst : PartialOrder α], IsGreatest s a → (Maximal (fun x => x ∈ s) x ↔ x = a)

Defined in

Mathlib.Order.Minimal

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PartialOrder