instIsAntisymmSubset

Mathlib.Data.Set.Basic

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

English

Let S and T be subsets of some type α. If S ⊆ T and T ⊆ S, then S = T.

Русский

Пусть S и T — подмножества множества α. Если S ⊆ T и T ⊆ S, то S = T.

LaTeX

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

Lean4

instance : IsAntisymm (Set α) (· ⊆ ·) :=
  show IsAntisymm (Set α) (· ≤ ·) by infer_instance

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

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

Разделы

Аффилиация

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