Mathlib Map

Theorems · Theorem · combinatorics

Set.IsWF.min.congr_simp

∀ {α : Type u_2} [inst : Preorder α] {s s_1 : Set α} (e_s : s = s_1) (hs : s.IsWF) (hn : s.Nonempty),
  hs.min hn = ⋯.min ⋯
Defined in
Mathlib.Data.Finset.SMulAntidiagonal
Cited by
3 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

HahnSeries.orderTop_neg · cited by 6HahnSeries.orderTop_negHahnSeries.addOppositeEquiv_orderTop · cited by 2HahnSeries.addOppositeEqu…HahnSeries.order_neg · cited by 0HahnSeries.order_negSet · cited by 53352SetPreorder · cited by 7952PreorderSet.Nonempty · cited by 2627Set.NonemptySet.IsWF · cited by 47Set.IsWFSet.IsWF.min · cited by 47IsWF.minmin.congr_simpCITED BYCITES

Cites5

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
  • Preorderstatement and proof · cited by 7,952
  • Set.Nonemptystatement and proof · cited by 2,627
  • Set.IsWFstatement and proof · cited by 47
  • Set.IsWF.minstatement and proof · cited by 47

Cited by3

Results whose statement or proof uses this declaration.