ssubset_def

Mathlib.Data.Set.Basic

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

English

A is a strict subset of B iff A ⊆ B and B is not a subset of A.

Русский

Множество A является строгим подмножеством B тогда и только тогда, когда A ⊆ B и B не является подмножеством A.

LaTeX

$$$s\subset t \iff (s\subseteq t \land \neg (t\subseteq s))$$$

Lean4

@[grind =]
theorem ssubset_def : (s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s) :=
  rfl

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

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

Разделы

Аффилиация

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