notMem_mono

Mathlib.Data.Finset.Defs

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

English

Let s ⊆ t and a ∉ t. Then a ∉ s.

Русский

Пусть s ⊆ t и a ∉ t. Тогда a ∉ s.

LaTeX

$$$\forall s,t:\ Finset\ α,\ \forall a:\alpha,\ s \subseteq t \to a \notin t \to a \notin s$$$

Lean4

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

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

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

Разделы

Аффилиация

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