isAsymm_of_isTrans_of_isIrrefl — Mathlib

English

If r is transitive and irreflexive, then r is asymmetric: whenever a ≺ b, then not b ≺ a.

Русский

Если r транзитивно и иррефлексивно, то r асимметрично: если a ≺ b, то не b ≺ a.

LaTeX

$$$(IsTrans\,\alpha\, r) \land (IsIrrefl\,\alpha\, r) \Rightarrow \forall a,b:\alpha, r a b \rightarrow \neg r b a$$$

Lean4

instance (priority := 90) isAsymm_of_isTrans_of_isIrrefl [IsTrans α r] [IsIrrefl α r] : IsAsymm α r :=
  ⟨fun a _b h₁ h₂ => absurd (_root_.trans h₁ h₂) (irrefl a)⟩

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