Remove `IsConnected` class.
parent
668c005c91
commit
e6a9504a8f
|
@ -1,4 +1,3 @@
|
||||||
import Common.Algebra
|
|
||||||
import Common.Finset
|
import Common.Finset
|
||||||
import Common.List
|
import Common.List
|
||||||
import Common.Logic
|
import Common.Logic
|
||||||
|
|
|
@ -1 +0,0 @@
|
||||||
import Common.Algebra.Classes
|
|
|
@ -1,13 +0,0 @@
|
||||||
import Mathlib.Init.Algebra.Classes
|
|
||||||
|
|
||||||
/-! # Common.Algebra.Classes
|
|
||||||
|
|
||||||
Additional theorems and definitions useful in the context of algebraic classes.
|
|
||||||
-/
|
|
||||||
|
|
||||||
/--
|
|
||||||
`IsConnected X lt` means that the binary relation `lt` on `X` is connected, that
|
|
||||||
is, either `lt a b` or `lt b a` for any distinct `a` and `b`.
|
|
||||||
-/
|
|
||||||
class IsConnected (α : Type u) (lt : α → α → Prop) : Prop where
|
|
||||||
connected : ∀ a b, a ≠ b → lt a b ∨ lt b a
|
|
Loading…
Reference in New Issue