instHasSSubset

Mathlib.Data.Finset.Defs

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

English

On Finset α, the strict subset relation s ⊂ t is defined by s ⊆ t and not t ⊆ s.

Русский

На Finset α строгая подмножество определяется как s ⊆ t и не t ⊆ s.

LaTeX

$$instance : HasSSubset (Finset α) := ⟨fun s t => s ⊆ t ∧ ¬ t ⊆ s⟩$$

Lean4

instance : HasSSubset (Finset α) :=
  ⟨fun s t => s ⊆ t ∧ ¬t ⊆ s⟩

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

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

Разделы

Аффилиация

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