ofUpperSet_le_ofUpperSet — Mathlib

English

The order on WithUpperSet α corresponds to the reverse order on α via the lower/upper set embeddings; specifically, for a,b, ofUpperSet a ≤ ofUpperSet b iff b ⤳ a.

Русский

Порядок на WithUpperSet α соответствует обратному порядку на α через отображения верхних/нижних множеств; например, a ≤ b в WithUpperSet эквивалентно b ⤳ a.

LaTeX

$$$\\forall a,b:\\mathrm{WithUpperSet}(\\alpha),\\; \\mathrm{ofUpperSet}(a) \\le \\mathrm{ofUpperSet}(b) \\iff b \\curvearrowright a.$$$

Lean4

@[simp]
theorem ofUpperSet_le_ofUpperSet {a b : WithUpperSet α} : ofUpperSet a ≤ ofUpperSet b ↔ b ⤳ a :=
  toUpperSet_specializes_toUpperSet.symm

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