eq_or_ssubset_of_subset

Mathlib.Data.Set.Basic

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

English

If S ⊆ T, then either S = T or S ⊂ T.

Русский

Если S ⊆ T, то либо S = T, либо S ⊂ T.

LaTeX

$$$\\forall S,T\\subseteq\\alpha, S\\subseteq T \\Rightarrow (S=T) \\lor (S\\subset T)$$$

Lean4

protected theorem eq_or_ssubset_of_subset (h : s ⊆ t) : s = t ∨ s ⊂ t :=
  eq_or_lt_of_le h

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

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

Разделы

Аффилиация

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