val_le_iff — Mathlib

English

The order on Finset α induced by its multiset representation corresponds to subset inclusion.

Русский

Порядок на Finset α, заданный через его представление как мультимножество, соответствует включению в подмножество.

LaTeX

$$$s_1.1 \le s_2.1 \iff s_1 \subseteq s_2$$$

Lean4

@[simp]
theorem val_le_iff {s₁ s₂ : Finset α} : s₁.1 ≤ s₂.1 ↔ s₁ ⊆ s₂ :=
  le_iff_subset s₁.2

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