notMem_mono

Mathlib.Data.Multiset.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.notMem_mono

English

If s ⊆ t and a ∉ t, then a ∉ s.

Русский

Если s ⊆ t и a ∉ t, то и a ∉ s.

LaTeX

$$$$s \subseteq t \Rightarrow a \notin t \Rightarrow a \notin s$$$$

Lean4

theorem notMem_mono (h : s ⊆ t) : a ∉ t → a ∉ s :=
  mt <| @h _

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

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

Разделы

Аффилиация

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