Theorems · Theorem · order theory

Set.maximal_iff_forall_insert

∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s) → (Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s))

Defined in

Mathlib.Order.Minimal

Cited by

3 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound