English
There is an order isomorphism sumLexDualAntidistrib between the dual of the lexicographic sum and the lexicographic sum of duals with swapped factors: (α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ.
Русский
Существует изоморфизм порядка sum Lex Dual Antidistrib между двойственным лексикографическим суммированием и лексикографической суммой двойственных с поменянными слагаемыми.
LaTeX
$$$\\text{sumLexDualAntidistrib}_{\\alpha,\\beta} : (\\alpha \\oplus_{\\mathrm{lex}} \\beta)^{\\mathrm{op}} \\cong_o \\beta^{\\mathrm{op}} \\oplus_{\\mathrm{lex}} \\alpha^{\\mathrm{op}}$$$
Lean4
/-- `WithTop α` is order-isomorphic to `α ⊕ₗ PUnit`, by sending `⊤` to `Unit` and `↑a` to
`a`. -/
def orderIsoSumLexPUnit : WithTop α ≃o α ⊕ₗ PUnit :=
⟨(Equiv.optionEquivSumPUnit α).trans toLex, fun {a b} =>
by
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk, Lex.toLex_le_toLex, le_refl]
cases a <;> cases b
· simp only [lex_inr_inr, le_top]
· simp only [lex_inr_inl, false_iff]
exact not_top_le_coe _
· simp only [Lex.sep, le_top]
· simp only [lex_inl_inl, coe_le_coe]⟩
