instIsIrreflOfIsNonstrictStrictOrder

English

If s is derived as a subrelation of a nonstrict strict order r, then s is irrefl; that is, no element is related to itself under s.

Русский

Если $s$ задаётся как подпорядок к нестрогому строгому порядку $r$, то $s$ иррефлексивен: нет элемента, который связан с самим собой.

LaTeX

$$IsIrrefl α s$$

Lean4

instance {s : α → α → Prop} [IsNonstrictStrictOrder α r s] : IsIrrefl α s :=
  ⟨fun _ h => ((right_iff_left_not_left_of r s).1 h).2 ((right_iff_left_not_left_of r s).1 h).1⟩

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