Total ordering


Definition

$$\forall x,y \in S : x{\mathrel{R}}y \vee y{\mathrel{R}}x$$

Isabelle

Orderings.linorder_class.le_cases:
(?x ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\) ?P
Orderings.linorder_class.le_cases3:
(?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?z \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?x \(\Longrightarrow\) ?x ≤ ?z \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?x ≤ ?z \(\Longrightarrow\) ?z ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?z ≤ ?y \(\Longrightarrow\) ?y ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?y ≤ ?z \(\Longrightarrow\) ?z ≤ ?x \(\Longrightarrow\) ?P) \(\Longrightarrow\)
(?z ≤ ?x \(\Longrightarrow\) ?x ≤ ?y \(\Longrightarrow\) ?P) \(\Longrightarrow\) ?P