subset_cons

Mathlib.Data.Finset.Insert

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

English

If h : a ∉ s then s ⊆ s.cons a h.

Русский

Если a не принадлежит s, то s ⊆ s.cons a h.

LaTeX

$$$(h : a \notin s) : s \subseteq s.cons a h$$$

Lean4

theorem subset_cons (h : a ∉ s) : s ⊆ s.cons a h :=
  Multiset.subset_cons _ _

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

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

Разделы

Аффилиация

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