Zulip Chat Archive
Stream: Is there code for X?
Topic: total_on
Yaël Dillies (Sep 11 2021 at 10:25):
Do we something akin to directed_on for total relations? I'm looking for the condition ∀ x y ∈ s, r x y ∨ r y x where s : set α and r : α → α → Prop
Kevin Buzzard (Sep 11 2021 at 10:48):
I think this is usually called a chain when the relation gives a poset
Yaël Dillies (Sep 11 2021 at 10:54):
Ah yes of course! Don't mind me :smile:
Last updated: Dec 20 2023 at 11:08 UTC