toLowerSet_specializes_toLowerSet

English

For a,b in α, toLowerSet a ⤳ toLowerSet b iff a ≤ b.

Русский

Для a,b ∈ α отношение специализации между изображениями нижних множеств toLowerSet(a) и toLowerSet(b) эквивалентно a ≤ b.

LaTeX

$$$\\forall {a b : α},\\; toLowerSet(a) \\;⤳\\; toLowerSet(b) \\iff a \\le b.$$$

Lean4

@[simp]
theorem toLowerSet_specializes_toLowerSet {a b : α} : toLowerSet a ⤳ toLowerSet b ↔ a ≤ b := by
  simp_rw [specializes_iff_closure_subset, IsLowerSet.closure_singleton, Ici_subset_Ici, toLowerSet_le_iff]

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