instIsNonstrictStrictOrderLeLt — Mathlib

English

In a preorder α, the pair (≤, <) satisfy lt_iff_le_not_ge: for all a,b ∈ α, a < b ⇔ a ≤ b ∧ ¬(b ≤ a).

Русский

В предпорядке α пара отношений (≤, <) удовлетворяет эквивалентности a < b ⇔ a ≤ b и не (b ≤ a).

LaTeX

$$$\forall a,b \in \alpha,\ a < b \iff a \le b \land \neg (b \le a)$$$

Lean4

instance [Preorder α] : IsNonstrictStrictOrder α (· ≤ ·) (· < ·) :=
  ⟨@lt_iff_le_not_ge _ _⟩

Похожие утверждения