instHasSubset — Mathlib

English

There is a canonical subset relation on Finset α given by: s ⊆ t iff every element of s is an element of t.

Русский

Для Finset α существует каноническое отношение подмножества: s ⊆ t тогда и только если каждый элемент s принадлежит t.

LaTeX

$$instance : HasSubset (Finset α) := ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩$$

Lean4

instance : HasSubset (Finset α) :=
  ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩

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