We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 1532a50 commit 1e3a519Copy full SHA for 1e3a519
src/Relation/Binary/Definitions.agda
@@ -99,7 +99,7 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
99
Dense : Rel A ℓ → Set _
100
Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
101
102
--- Generalised connex - exactly one of the two relations holds.
+-- Generalised connex - at least one of the two relations holds.
103
104
Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _
105
Connex P Q = ∀ x y → P x y ⊎ Q y x
0 commit comments