erase_inf_Ici — Mathlib

English

Remove a from s and intersect with the ray Ici(a) recovers s under suitable conditions.

Русский

Удаление a из s и пересечение с ray Ici(a) восстанавливает s при определённых условиях.

LaTeX

$$$ s.erase a \\sqcap \\mathrm{Ici}(a) = s $$$

Lean4

theorem erase_inf_Ici (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : s.erase a ⊓ Ici a = s := by
  rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure] <;> simpa

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