Theorems · Theorem · order theory
minimal_subset_iff
∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s = t- Defined in
- Mathlib.Order.Minimal
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Minimalstatement · cited by 150
- minimal_iffproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- Matroid.isBase_iff_minimal_spanningproof · cited by 2
- Matroid.IsBase.compl_closure_sdiff_singleton_isCocircuitproof · cited by 1
- Matroid.Spanning.isBase_of_minimalproof · cited by 0