refactor: Remove duplicate definition of Antisymmetric (#183)

Foundation/IntProp/Kripke/Basic.lean

@@ -36,7 +36,7 @@ lemma rel_trans' : Transitive F.Rel := by apply rel_trans;
 lemma rel_refl' : Reflexive F.Rel := by apply rel_refl
 
 @[simp] lemma rel_antisymm {x y : F.World} : x ≺ y → y ≺ x → x = y := IsAntisymm.antisymm x y
-lemma rel_antisymm' : Antisymmetric F.Rel := by apply rel_antisymm
+lemma rel_antisymm' : AntiSymmetric F.Rel := by apply rel_antisymm
 
 end Frame
 

Foundation/Logic/Kripke/Basic.lean

@@ -124,7 +124,7 @@ abbrev TransitiveIrreflexiveFrameClass : FrameClass := { F | Transitive F ∧ Ir
 abbrev ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ WeaklyConverseWellFounded F }
 
 /-- FrameClass for `𝐆𝐫𝐳` (Finite version) -/
-abbrev ReflexiveTransitiveAntisymmetricFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ Antisymmetric F }
+abbrev ReflexiveTransitiveAntiSymmetricFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ AntiSymmetric F }
 
 end
 

Foundation/Modal/Boxdot/GL_Grz.lean

@@ -47,7 +47,7 @@ namespace Kripke
 open Relation (ReflGen)
 open Formula.Kripke
 
-lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈ TransitiveIrreflexiveFiniteFrameClass) : ⟨F.toFrame^=⟩ ∈ ReflexiveTransitiveAntisymmetricFiniteFrameClass := by
+lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈ TransitiveIrreflexiveFiniteFrameClass) : ⟨F.toFrame^=⟩ ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass := by
   obtain ⟨F_trans, F_irrefl⟩ := hF;
   refine ⟨?F_refl, ?F_trans, ?F_antisymm⟩;
   . intro x; apply ReflGen.refl;
@@ -65,7 +65,7 @@ lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈
       have := F_irrefl x;
       contradiction;
 
-lemma mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass (hF : F ∈ ReflexiveTransitiveAntisymmetricFiniteFrameClass) : ⟨F.toFrame^≠⟩ ∈ TransitiveIrreflexiveFiniteFrameClass := by
+lemma mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass (hF : F ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass) : ⟨F.toFrame^≠⟩ ∈ TransitiveIrreflexiveFiniteFrameClass := by
   obtain ⟨_, F_trans, F_antisymm⟩ := hF;
   refine ⟨?F_trans, ?F_irrefl⟩;
   . rintro x y z ⟨nexy, Rxy⟩ ⟨_, Ryz⟩;

Foundation/Modal/Kripke/Grz/Completeness.lean

@@ -76,7 +76,7 @@ lemma transitive : Transitive (miniCanonicalFrame φ).Rel := by
     subst_vars;
     tauto;
 
-lemma antisymm : Antisymmetric (miniCanonicalFrame φ).Rel := by
+lemma antisymm : AntiSymmetric (miniCanonicalFrame φ).Rel := by
   rintro X Y ⟨_, h₁⟩ ⟨h₂, _⟩;
   exact h₁ h₂;
 
@@ -257,7 +257,7 @@ lemma truthlemma {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformu
 
 open Modal.Kripke
 
-instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetricFiniteFrameClass) := ⟨by
+instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntiSymmetricFiniteFrameClass) := ⟨by
   intro φ;
   contrapose;
   intro h;
@@ -278,7 +278,7 @@ instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetric
       tauto;
 ⟩
 
-instance : Kripke.FiniteFrameProperty (Hilbert.Grz ℕ) ReflexiveTransitiveAntisymmetricFiniteFrameClass where
+instance : Kripke.FiniteFrameProperty (Hilbert.Grz ℕ) ReflexiveTransitiveAntiSymmetricFiniteFrameClass where
   complete := complete
   sound := finite_sound
 

Foundation/Modal/Kripke/Grz/Definability.lean

@@ -13,7 +13,7 @@ open Formula.Kripke
 open Relation (IrreflGen)
 
 abbrev ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel }
-abbrev ReflexiveTransitiveAntisymmetricFiniteFrameClass : FiniteFrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ Antisymmetric F.Rel }
+abbrev ReflexiveTransitiveAntiSymmetricFiniteFrameClass : FiniteFrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ AntiSymmetric F.Rel }
 
 variable {F : Kripke.Frame}
 
@@ -172,7 +172,7 @@ lemma ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz :
   . rintro h;
     refine ⟨refl_of_Grz h, trans_of_Grz h, WCWF_of_Grz h⟩;
 
-lemma ReflexiveTransitiveAntisymmetricFiniteFrameClass.is_defined_by_Grz : ReflexiveTransitiveAntisymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇 := by
+lemma ReflexiveTransitiveAntiSymmetricFiniteFrameClass.is_defined_by_Grz : ReflexiveTransitiveAntiSymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇 := by
   intro F;
   constructor;
   . rintro ⟨hRefl, hTrans, hAntisymm⟩;
@@ -196,12 +196,12 @@ open Hilbert.Kripke
 instance Grz.Kripke.sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass) :=
   instSound_of_frameClass_definedBy ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz rfl
 
-instance Grz.Kripke.finite_sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetricFiniteFrameClass) :=
-  instSound_of_finiteFrameClass_definedBy ReflexiveTransitiveAntisymmetricFiniteFrameClass.is_defined_by_Grz rfl
+instance Grz.Kripke.finite_sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveAntiSymmetricFiniteFrameClass) :=
+  instSound_of_finiteFrameClass_definedBy ReflexiveTransitiveAntiSymmetricFiniteFrameClass.is_defined_by_Grz rfl
 
-instance Grz.consistent : System.Consistent (Hilbert.Grz ℕ) := Kripke.instConsistent_of_nonempty_finiteFrameclass (FC := ReflexiveTransitiveAntisymmetricFiniteFrameClass) $ by
+instance Grz.consistent : System.Consistent (Hilbert.Grz ℕ) := Kripke.instConsistent_of_nonempty_finiteFrameclass (FC := ReflexiveTransitiveAntiSymmetricFiniteFrameClass) $ by
   use reflexivePointFrame;
-  simp [Transitive, Reflexive, Antisymmetric];
+  simp [Transitive, Reflexive, AntiSymmetric];
 
 end Hilbert
 

Foundation/Vorspiel/BinaryRelations.lean

@@ -25,8 +25,6 @@ def Coreflexive := ∀ ⦃x y⦄, x ≺ y → x = y
 
 def Equality := ∀ ⦃x y⦄, x ≺ y ↔ x = y
 
-def Antisymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
-
 def Isolated := ∀ ⦃x y⦄, ¬(x ≺ y)
 
 def Assymetric := ∀ ⦃x y⦄, (x ≺ y) → ¬(y ≺ x)
@@ -72,7 +70,7 @@ lemma refl_of_symm_serial_eucl (hSymm : Symmetric rel) (hSerial : Serial rel) (h
   have Ryx := hSymm Rxy;
   exact trans_of_symm_eucl hSymm hEucl Rxy Ryx;
 
-lemma corefl_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Coreflexive rel := by
+lemma corefl_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : AntiSymmetric rel) (hEucl : Euclidean rel) : Coreflexive rel := by
   intro x y Rxy;
   have Ryx := hEucl (hRefl x) Rxy;
   exact hAntisymm Rxy Ryx;
@@ -83,7 +81,7 @@ lemma equality_of_refl_corefl (hRefl : Reflexive rel) (hCorefl : Coreflexive rel
   . apply hCorefl;
   . rintro rfl; apply hRefl;
 
-lemma equality_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Equality rel := by
+lemma equality_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : AntiSymmetric rel) (hEucl : Euclidean rel) : Equality rel := by
   apply equality_of_refl_corefl;
   . assumption;
   . exact corefl_of_refl_assym_eucl hRefl hAntisymm hEucl;
@@ -163,9 +161,9 @@ lemma Finite.exists_ne_map_eq_of_infinite_lt {α β} [LinearOrder α] [Infinite
     . contradiction;
     . use j, i; simp [hij, e];
 
-lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → Antisymmetric R := by
+lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → AntiSymmetric R := by
   contrapose;
-  simp [Antisymmetric];
+  simp [AntiSymmetric];
   intro x y Rxy Ryz hxy;
   apply ConverseWellFounded.iff_has_max.not.mpr;
   push_neg;
@@ -178,15 +176,15 @@ lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → Antisymmetric R :=
     . use x; simp_all [Relation.IrreflGen];
 
 lemma WCWF_of_finite_trans_antisymm {R : α → α → Prop} (hFin : Finite α) (R_trans : Transitive R)
-  : Antisymmetric R → WCWF R := by
+  : AntiSymmetric R → WCWF R := by
     contrapose;
     intro hWCWF;
     replace hWCWF := ConverseWellFounded.iff_has_max.not.mp hWCWF;
     push_neg at hWCWF;
     obtain ⟨f, hf⟩ := dependent_choice hWCWF; clear hWCWF;
     simp [Relation.IrreflGen] at hf;
 
-    simp [Antisymmetric];
+    simp [AntiSymmetric];
     obtain ⟨i, j, hij, e⟩ := Finite.exists_ne_map_eq_of_infinite_lt f;
     use (f i), (f (i + 1));
     have ⟨hi₁, hi₂⟩ := hf i;