directedOn_pair — Mathlib

English

If a ≤ b (a ≼ b) and r is directed, then {a,b} is directed.

Русский

Если a ≤ b и r направлена, то множество {a,b} направлено.

LaTeX

$$$\text{DirectedOn}(r, \{a,b\})$ при условии $a \preceq b$ и рефлексивности.$$

Lean4

theorem directedOn_pair (h : Reflexive r) {a b : α} (hab : a ≼ b) : DirectedOn r ({ a, b } : Set α) :=
  (directedOn_singleton h _).insert h _ fun c hc => ⟨c, hc, hc.symm ▸ hab, h _⟩

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