Zulip Chat Archive
Stream: Is there code for X?
Topic: Chains of irreflexive relation is Finite
SnO2WMaN (Jul 18 2024 at 13:04):
I am looking for / want to prove that "there are at most finite number of chains by ireflexive and transitive relations on finite elements". Roughly speaking, there are at most |α|! (|α| is number of elements), so might be obviously, but if you can think of a simple proof, please let me know.
import Mathlib.Init.Logic
import Mathlib.Data.Finite.Defs
theorem List.chains_finite [Finite α] {R : α → α → Prop} (R_trans : Transitive R) (R_irrefl : Irreflexive R) : Finite { l : List α // l.Chain' R } := by
sorry;
Floris van Doorn (Jul 18 2024 at 13:20):
Please edit your post to include a full #mwe with imports/variables
Floris van Doorn (Jul 18 2024 at 13:22):
It seems false if R is not transitive: Can't [a,b,a,b,a,b,a,b] be part of your subtype?
SnO2WMaN (Jul 18 2024 at 13:24):
Sorry I made mistake, thanks for advice.
SnO2WMaN (Jul 18 2024 at 13:29):
Added mwe.
Floris van Doorn (Jul 18 2024 at 13:37):
I recommend proving { l : List α | l.Nodup }.Finite and l.Chain' R → l.Nodup
SnO2WMaN (Jul 21 2024 at 06:02):
Thanks @Floris van Doorn , I proved.
I think this lemma might be useful in as if there's in Mathlib, How's about?
import Mathlib.Init.Logic
import Mathlib.Data.Finite.Defs
import Mathlib.Data.List.Duplicate
import Mathlib.Data.List.Chain
import Mathlib.Data.Fintype.List
import Mathlib.Data.Fintype.Card
variable {l l₁ l₂ : List α}
variable {R : α → α → Prop}
lemma Chain'.nodup_of_trans_irreflex (R_trans : Transitive R) (R_irrefl : Irreflexive R) (h_chain : l.Chain' R) : l.Nodup := by
by_contra hC;
replace ⟨d, hC⟩ := List.exists_duplicate_iff_not_nodup.mpr hC;
have := List.duplicate_iff_sublist.mp hC;
have := @List.Chain'.sublist α R [d, d] l ⟨by aesop⟩ h_chain this;
simp at this;
exact R_irrefl d this;
instance finiteNodupList [DecidableEq α] [Finite α] : Finite { l : List α // l.Nodup } := @fintypeNodupList α _ (Fintype.ofFinite α) |>.finite
lemma chains_finite [DecidableEq α] [Finite α] (R_trans : Transitive R) (R_irrefl : Irreflexive R) : Finite { l : List α // l.Chain' R } := by
apply @Finite.of_injective { l : List α // l.Chain' R } { l : List α // l.Nodup } _ ?f;
case f => intro ⟨l, hl⟩; refine ⟨l, List.Chain'.nodup_of_trans_irreflex R_trans R_irrefl hl⟩;
simp [Function.Injective];
Last updated: May 02 2025 at 03:31 UTC