toUpperSet_specializes_toUpperSet

English

For a,b in α, the specialization relation between their upper-set images satisfies toUpperSet(a) ⤳ toUpperSet(b) iff b ≤ a.

Русский

Для a,b в α специальностная связь между верхними множествами toUpperSet(a) и toUpperSet(b) равна тогда и только тогда, когда b ≤ a.

LaTeX

$$$\\mathrm{toUpperSet}(a) \\;\\,\\!⤳\\;\\mathrm{toUpperSet}(b) \\iff b \\le a$$$

Lean4

@[simp]
theorem toUpperSet_specializes_toUpperSet {a b : α} : toUpperSet a ⤳ toUpperSet b ↔ b ≤ a := by
  simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic, toUpperSet_le_iff]

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