ofLowerSet_le_ofLowerSet — Mathlib

English

For a,b in WithLowerSet α, ofLowerSet a ≤ ofLowerSet b iff a ⤳ b.

Русский

Для a,b в WithLowerSet α выполняется a ⤳ b тогда и только тогда, когда ofLowerSet(a) ≤ ofLowerSet(b).

LaTeX

$$$\\forall {a b : WithLowerSet \\alpha},\\; ofLowerSet(a) \\le ofLowerSet(b) \\iff a \\curvearrowright b.$$$

Lean4

@[simp]
theorem ofLowerSet_le_ofLowerSet {a b : WithLowerSet α} : ofLowerSet a ≤ ofLowerSet b ↔ a ⤳ b :=
  toLowerSet_specializes_toLowerSet.symm

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