instLE

Mathlib.Data.Set.Defs

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

English

The order ≤ on sets is defined by ⊆.

Русский

Порядок ≤ на множествах задан как ⊆.

LaTeX

$$$s \\le t \\iff s \\subseteq t$$$

Lean4

/-- We introduce `≤` before `⊆` to help the unifier when applying lattice theorems
to subset hypotheses. -/
instance : LE (Set α) :=
  ⟨Set.Subset⟩

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

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

Разделы

Аффилиация

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