erase_sup_Iic — Mathlib

English

Let s be a lower set and a ∈ s, and assume that for all b ∈ s, a ≤ b implies b = a. Then s.erase a joined with Iic(a) equals s.

Русский

Пусть s — нижнее множество, a ∈ s, и пусть для всех b ∈ s верно: a ≤ b ⇒ b = a. Тогда s.erase a объединённое с Iic(a) даёт s.

LaTeX

$$$ (s \\setminus \\{a\\}) \\sqcup \\operatorname{Iic}(a) = s $$$

Lean4

theorem erase_sup_Iic (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : s.erase a ⊔ Iic a = s := by
  rw [← lowerClosure_singleton, ← sdiff_singleton, sdiff_sup_lowerClosure] <;> simpa

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