English
For a finite linearly ordered α and m,n with a subset s of cardinality m and its complement of cardinality n, there is an order isomorphism Fin m ⊕ Fin n ≃ α, sending Fin m to s and Fin n to sᶜ in order.
Русский
Для конечного линейно упорядоченного α и чисел m,n с подмножество s размера m и дополнение sᶜ размера n существует порядковый изоморфизм Fin m ⊕ Fin n ≃ α, который отображает Fin m в s, Fin n в sᶜ в порядке.
LaTeX
$$$Fin m \oplus Fin n \cong_o α$$$
Lean4
/-- If `α` is a linearly ordered fintype, `s : Finset α` has cardinality `m` and its complement has
cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of `Fin m` to
elements of `s` and elements of `Fin n` to elements of `sᶜ` while preserving order on each
"half" of `Fin m ⊕ Fin n` (using `Set.orderIsoOfFin`). -/
def finSumEquivOfFinset (hm : #s = m) (hn : #sᶜ = n) : Fin m ⊕ Fin n ≃ α :=
calc
Fin m ⊕ Fin n ≃ (s : Set α) ⊕ (sᶜ : Set α) :=
Equiv.sumCongr (s.orderIsoOfFin hm).toEquiv <| (sᶜ.orderIsoOfFin hn).toEquiv.trans <| Equiv.setCongr s.coe_compl
_ ≃ α := Equiv.Set.sumCompl _
