ssubset_cons

Mathlib.Data.Finset.Insert

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

English

For h : a ∉ s, we have s ⊂ s.cons a h.

Русский

Если a не принадлежит s, тогда s является строгим подмножеством s.cons a h.

LaTeX

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

Lean4

theorem ssubset_cons (h : a ∉ s) : s ⊂ s.cons a h :=
  Multiset.ssubset_cons h

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

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

Разделы

Аффилиация

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