Dirac's lemma, strong form: in a chordless-cycle-free adjacency structure, every vertex set is a clique or contains two nonadjacent simplicial vertices.
DeclHiddenChannelCapacity.dirac_strong
∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
(¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
∀ (S : Finset ι),
(∀ x ∈ S, ∀ y ∈ S, x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) ∨
∃ u w,
HiddenChannelCapacity.SimpIn 𝒞 S u ∧
HiddenChannelCapacity.SimpIn 𝒞 S w ∧ u ≠ w ∧ ¬HiddenChannelCapacity.Adj 𝒞 u wTopicGraphical models
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6020 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6020
Cite
Verification
- Library
- ZPM.Measurements.HC.Dirac
- Statement digest
- e606da67595a
- First verified
- 2026-09-24T00:00:00Z