Theorems · Theorem · order theory
IsAntichain.eq
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → ∀ {a b : α}, a ∈ s → b ∈ s → r a b → a = b- Defined in
- Mathlib.Order.Antichain
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 16 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
- IsAntichainstatement and proof · cited by 105
- Set.Pairwise.eqproof · cited by 12
Cited by13
Results whose statement or proof uses this declaration.
- IsAntichain.finite_of_partiallyWellOrderedOnproof · cited by 6
- isAntichain_and_greatest_iffproof · cited by 2
- IsAntichain.eq'proof · cited by 2
- IsAntichain.eq_setOfPred_maximalproof · cited by 2
- IsAntichain.subsingletonproof · cited by 1
- Finset.truncatedInf_of_isAntichainproof · cited by 1
- IsAntichain.minimal_mem_iffproof · cited by 1
- IsAntichain.minimal_mem_upperClosure_iff_memproof · cited by 1
- IsAntichain.ordConnectedproof · cited by 1
- IsAntichain.finite_of_wellQuasiOrderedproof · cited by 1
- Finset.truncatedSup_of_isAntichainproof · cited by 0
- IsAntichain.antisymmproof · cited by 0