Theorems · Theorem · order theory
Set.IsWF.min_union
∀ {α : Type u_2} [inst : LinearOrder α] {s t : Set α} (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty),
⋯.min ⋯ = min (hs.min hsn) (ht.min htn)- Defined in
- Mathlib.Order.WellFoundedSet
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- LinearOrderstatement and proof · cited by 8,572
- Set.Nonemptystatement and proof · cited by 2,627
- le_antisymmproof · cited by 2,068
- Set.subset_union_leftproof · cited by 142
- Set.subset_union_rightproof · cited by 123
- Set.IsWFstatement and proof · cited by 47
- Set.IsWF.minstatement and proof · cited by 47
- Set.mem_unionproof · cited by 47
- le_minproof · cited by 21
- Set.IsWF.min_memproof · cited by 20
- min_le_iffproof · cited by 15
Cited by1
Results whose statement or proof uses this declaration.
- HahnSeries.min_le_min_addproof · cited by 2