erase_covBy

Mathlib.Data.Finset.Grade

URI: https://scilib.ai/kg/mathlib#Finset.erase_covBy

English

If a ∈ s, then s.erase a is covered by s.

Русский

Если a ∈ s, то s.erase a покрыто по отношению к s.

LaTeX

$$$ (ha : a \in s) \Rightarrow s.erase a \covBy s $$$

Lean4

@[simp]
theorem erase_covBy (ha : a ∈ s) : s.erase a ⋖ s :=
  ⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩

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

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

Разделы

Аффилиация

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