isWellFounded_ssubset — Mathlib

English

The strict subset relation on multisets is well-founded; every nonempty multiset has a minimal element under ⊂.

Русский

Строгое подмножество на мультимножества образует хорошо упорядоченность; каждое непустое мультимножество имеет минимальный элемент относительно ⊂.

LaTeX

$$$\\text{IsWellFounded}(\\mathsf{Multiset}\\,\\beta, \\\\subset)$$$$

Lean4

instance isWellFounded_ssubset : IsWellFounded (Multiset β) (· ⊂ ·) := by
  classical exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

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