subset_def — Mathlib

English

Subset relation on Finset is equivalent to the subset relation on the underlying multisets of elements.

Русский

Отношение подмножества на Finset эквивалентно соответствующему отношению подмножества для сопутствующих мультисет элементов.

LaTeX

$$theorem subset_def : s ⊆ t ↔ s.1 ⊆ t.1 := Iff.rfl$$

Lean4

theorem subset_def : s ⊆ t ↔ s.1 ⊆ t.1 :=
  Iff.rfl

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