nontrivial_mono

Mathlib.Data.Set.Subsingleton

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

← MathLib Explorer

English

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

Русский

Если s ⊆ t и s не тривиально, то и t не тривиально.

LaTeX

$$s ⊆ t \Rightarrow s.Nontrivial \Rightarrow t.Nontrivial$$

Lean4

theorem nontrivial_mono {α : Type*} {s t : Set α} (hst : s ⊆ t) (hs : Nontrivial s) : Nontrivial t :=
  Nontrivial.coe_sort <| (nontrivial_coe_sort.1 hs).mono hst

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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