val_lt_iff — Mathlib

English

The subset relation after coercion to sets coincides with the Finset subset relation.

Русский

Отношение подмножества после перевода в множества совпадает с отношением подмножества для Finset.

LaTeX

$$$Set.instHasSubset.Subset s_1.toSet s_2.toSet \iff Finset.instHasSubset.Subset s_1 s_2$$$

Lean4

@[simp]
theorem val_lt_iff {s₁ s₂ : Finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
  and_congr val_le_iff <| not_congr val_le_iff

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