covBy_iff_exists_sdiff_singleton

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#Set.covBy_iff_exists_sdiff_singleton

← MathLib Explorer

English

If s ⋖ t, there exists an element a ∈ t with t \ {a} = s.

Русский

Если s покрыто t, существует a ∈ t такой, что t \ {a} = s.

LaTeX

$$$ s \covBy t \Rightarrow \exists a \in t,\; t \setminus \{a\} = s $$$

Lean4

theorem covBy_iff_exists_sdiff_singleton : s ⋖ t ↔ ∃ a ∈ t, t \ { a } = s :=
  ⟨CovBy.exists_set_sdiff_singleton, by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covBy ha⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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