mono

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.mono

English

If s ⊆ t and s is nonempty, then t is nonempty.

Русский

Если s ⊆ t и s непусто, тогда t непусто.

LaTeX

$$$s \\\\subseteq t \\\\wedge s \\\\neq \\\\emptyset \\\\Rightarrow t \\\\neq \\\\emptyset$$$

Lean4

@[gcongr]
theorem mono {s t : Finset α} (hst : s ⊆ t) (hs : s.Nonempty) : t.Nonempty :=
  Set.Nonempty.mono hst hs

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

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

Разделы

Аффилиация

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