notMem_subset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.notMem_subset

English

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

Русский

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

LaTeX

$$$\\forall {s,t:Set\\alpha} (h: s\\subset t), a\\notin t \\Rightarrow a\\notin s$$$

Lean4

theorem notMem_subset (h : s ⊆ t) : a ∉ t → a ∉ s :=
  mt <| mem_of_subset_of_mem h

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

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

Разделы

Аффилиация

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