Ici_inf_erase

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_inf_erase

English

The dual equality to erase_inf_Ici: Ici(a) ∩ s.erase a = s under the same assumptions.

Русский

Дуальное равенство erase_inf_Ici: Ici(a) ∩ s.erase a = s при тех же предположениях.

LaTeX

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

Lean4

theorem Ici_inf_erase (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : Ici a ⊓ s.erase a = s := by
  rw [inf_comm, erase_inf_Ici ha has]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru