exists_finset_erase

Mathlib.Data.Finset.Grade

URI: https://scilib.ai/kg/mathlib#CovBy.exists_finset_erase

← MathLib Explorer

English

If s ⋖ t then there exists a ∈ t such that t.erase a = s.

Русский

Если s ⋖ t, то существует a ∈ t такое, что t.erase a = s.

LaTeX

$$$ h : s \covBy t \Rightarrow \exists a \in t, t.erase a = s $$$

Lean4

theorem _root_.CovBy.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by
  simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton

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

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

Разделы

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

Аффилиация

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