Iic_sup_erase — Mathlib

English

Let s be a lower set and a ∈ s with ∀ b ∈ s, a ≤ b → b = a. Then Iic(a) joined with s.erase a yields s.

Русский

Пусть s — нижнее множество, a ∈ s и выполняется ∀ b ∈ s, a ≤ b → b = a. Тогда Iic(a) ⊔ s.erase a = s.

LaTeX

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

Lean4

theorem Iic_sup_erase (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : Iic a ⊔ s.erase a = s := by
  rw [sup_comm, erase_sup_Iic ha has]

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