instIsAsymmSSubset

Mathlib.Data.Set.Basic

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

English

If S ⊊ T, then not (T ⊊ S).

Русский

Если S ⊊ T, то недопустимо T ⊊ S.

LaTeX

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

Lean4

instance : IsAsymm (Set α) (· ⊂ ·) :=
  show IsAsymm (Set α) (· < ·) by infer_instance

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

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

Разделы

Аффилиация

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