isDirected_ge — Mathlib

English

If a set A is directed under ≤, then the opposite order A^{op} is directed under ≥.

Русский

Если множество A направлено относительно ≤, то в противоположном порядке A^{op} направлено относительно ≥.

LaTeX

$$$IsDirected(\alpha, \le) \rightarrow IsDirected(\alpha^{\mathrm{op}}, \ge)$$$

Lean4

instance isDirected_ge [LE α] [IsDirected α (· ≤ ·)] : IsDirected αᵒᵈ (· ≥ ·) := by assumption

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