ordConnected_range_val — Mathlib

English

Finite sets form an order-connected suborder of multisets: the image of Finset α inside Multiset α is order-connected.

Русский

Множества с конечной кардинальностью образуют заказанно-связанный подпорядок над мультсетами; изображение Finset α внутри Multiset α является упорядочно-связанным.

LaTeX

$$$ \operatorname{Set}.OrdConnected(\operatorname{Set.range}(\operatorname{val}:\ Finset\alpha \to\ Multiset\alpha))$$$

Lean4

/-- Finsets form an order-connected suborder of multisets. -/
theorem ordConnected_range_val : Set.OrdConnected (Set.range val : Set <| Multiset α) :=
  ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩⟩

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