zero_ssubset

Mathlib.Data.Multiset.ZeroCons

URI: https://scilib.ai/kg/mathlib#Multiset.zero_ssubset

English

0 is a strict subset of s if and only if s ≠ 0.

Русский

0 является строгим подмножеством s тогда и только тогда, когда s ≠ 0.

LaTeX

$$$0 \\subsetneq s \\iff s \\neq 0$$$

Lean4

@[simp]
theorem zero_ssubset : 0 ⊂ s ↔ s ≠ 0 := by simp [ssubset_iff_subset_not_subset]

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

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

Разделы

Аффилиация

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