Covering relation

Stream: Is there code for X?

[Yaël Dillies]

Do we agree that we don't have the covering relation?

variables {α : Type*}

def covers [has_le α] (a b : α) : Prop := a ≤ b ∧ ∀ ⦃c⦄, a ≤ c → ¬ c ≤ b

[Yury G. Kudryashov]

variables {α : Type*}

def covers [has_le α] (a b : α) : Prop := a ≤ b ∧ ∀ ⦃c⦄, a ≤ c → ¬ c ≤ b

lemma not_covers [preorder α] (a b : α) (h : covers a b) : false :=
begin
  cases h with hle h,
  apply h hle,
  refl
end

[Yury G. Kudryashov]

So, with this definition we have it, and it is called λ _ _, false.

[Yaël Dillies]

Whoops sorry! I obviously meant < :sweat_smile: