mono

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.mono

English

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

Русский

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

LaTeX

$$$ \text{Nontrivial}(s) \wedge s \subseteq t \Rightarrow \text{Nontrivial}(t) $$$

Lean4

theorem mono (hs : s.Nontrivial) (hst : s ⊆ t) : t.Nontrivial :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, hst hx, y, hst hy, hxy⟩

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

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

Разделы

Аффилиация

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