Order Theory - POsets - a specific subset Definition

Stream: maths

[Abraham Solomon]

Hey all,

I am new to order theory, i am trying to use something used in studying trees as graphs.

Essentially its finite sets of vertices where every ray from the root must intersect them at least once. These are typically called cutsets.

In order theory, given $(P,\leq)$ with a least element 0(root for a tree) , $X \subset P$ would be a ' cutset ' if its finite and every element in $P \setminus X$ is comparable to some element in $X$(they need not be comparable to each other within $X$). Or perhaps every chain (ray) starting from 0 intersects this set.

Is there a definition for this in order theory? I couldn't find it on https://en.wikipedia.org/wiki/Glossary_of_order_theory

[Daniel Weber]

There was a discussion about cutsets in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Code.20for.20studying.20infinite.20rooted.20trees

[Abraham Solomon]

Daniel Weber said:

There was a discussion about cutsets in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Code.20for.20studying.20infinite.20rooted.20trees

Yea that was me too, and you were actually very helpful for how to treat it in Lean 4 in that thread thank you :smiling_face:

I was just curious if order theory already had their own word for it , and perhaps even associated theorems.