exists_finset_insert

Mathlib.Data.Finset.Grade

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

English

If s ⋖ t then there exists a ∉ s with insert a s = t.

Русский

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

LaTeX

$$$ h : s \covBy t \Rightarrow \exists a \; \exists ha:\ a \notin s \land (\operatorname{insert} a\ s) = t $$$

Lean4

theorem _root_.CovBy.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by simpa using h.exists_finset_cons

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

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

Разделы

Аффилиация

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