nonempty_of_not_subset

Mathlib.Data.Set.Basic

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

English

If S ⊆ T and S is nonempty, then T is nonempty.

Русский

Если S ⊆ T и S непусто, то T непусто.

LaTeX

$$$(s \subseteq t) \Rightarrow (s.Nonempty \Rightarrow t.Nonempty)$$$

Lean4

theorem nonempty_of_not_subset (h : ¬s ⊆ t) : (s \ t).Nonempty :=
  let ⟨x, xs, xt⟩ := not_subset.1 h
  ⟨x, xs, xt⟩

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

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

Разделы

Аффилиация

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