instIsAntisymmSubset

Mathlib.Data.Finset.Defs

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

English

Subset is antisymmetric: if s ⊆ t and t ⊆ s then s = t.

Русский

Подмножество антисимметрично: если s ⊆ t и t ⊆ s, то s = t.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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