From e6a9504a8fe7d4054c4bf9266c7f847bd6d2a928 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 15 Jul 2023 15:05:45 -0600 Subject: [PATCH] Remove `IsConnected` class. --- Common.lean | 1 - Common/Algebra.lean | 1 - Common/Algebra/Classes.lean | 13 ------------- 3 files changed, 15 deletions(-) delete mode 100644 Common/Algebra.lean delete mode 100644 Common/Algebra/Classes.lean diff --git a/Common.lean b/Common.lean index 39037ec..dc64440 100644 --- a/Common.lean +++ b/Common.lean @@ -1,4 +1,3 @@ -import Common.Algebra import Common.Finset import Common.List import Common.Logic diff --git a/Common/Algebra.lean b/Common/Algebra.lean deleted file mode 100644 index 46d0ab1..0000000 --- a/Common/Algebra.lean +++ /dev/null @@ -1 +0,0 @@ -import Common.Algebra.Classes \ No newline at end of file diff --git a/Common/Algebra/Classes.lean b/Common/Algebra/Classes.lean deleted file mode 100644 index 21ef4c7..0000000 --- a/Common/Algebra/Classes.lean +++ /dev/null @@ -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 \ No newline at end of file