erase_lt

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#LowerSet.erase_lt

English

s.erase(a) < s iff a ∈ s.

Русский

s.erase(a) < s тогда и только тогда, когда a ∈ s.

LaTeX

$$$ s.erase(a) < s \\iff a \\in s $$$

Lean4

@[simp]
theorem erase_lt : s.erase a < s ↔ a ∈ s :=
  erase_le.lt_iff_ne.trans erase_eq.not_left

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

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

Разделы

Аффилиация

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