ordConnected_range_coe — Mathlib

English

The set of finite subsets of α, viewed as ordinary sets via the embedding into the power set, is order-connected in the inclusion order.

Русский

Множество конечных подмножеств α, воспринятое как подмножество множества подмножеств по включению, образует упорядочно-связанную структуру.

LaTeX

$$$(\text{Set.range }(\uparrow):\ Finset\alpha \to\ Set\alpha).\operatorname{OrdConnected}$$$

Lean4

/-- Finsets form an order-connected suborder of sets. -/
theorem ordConnected_range_coe : Set.OrdConnected (Set.range ((↑) : Finset α → Set α)) :=
  ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩⟩

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