English
There is an order isomorphism that describes how the dual of a lexicographic sum behaves under swapping the factors: (α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ.
Русский
Существуют два взаимно-обратно-распределяющих порядка представления, описывающие как двойственный оператор над лексикографической суммой ведёт себя при смене слагаемых: (α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ.
LaTeX
$$$ (\\alpha \\oplus_{\\mathrm{lex}} \\beta)^{\\mathrm{op}} \\cong_o \\beta^{\\mathrm{op}} \\oplus_{\\mathrm{lex}} \\alpha^{\\mathrm{op}} $$$
Lean4
/-- `OrderDual` is antidistributive over `⊕ₗ` up to an order isomorphism. -/
def sumLexDualAntidistrib (α β : Type*) [LE α] [LE β] : (α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ :=
{ Equiv.sumComm α β with
map_rel_iff' := fun {a b} => by
rcases a with (a | a) <;> rcases b with (b | b)
· simp only [ge_iff_le]
change toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔ toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
simp [toDual_le_toDual]
· exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _) Lex.not_inr_le_inl
· exact iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) (Lex.inl_le_inr _ _)
· change toLex (inl <| toDual a) ≤ toLex (inl <| toDual b) ↔ toDual (toLex <| inr a) ≤ toDual (toLex <| inr b)
simp [toDual_le_toDual] }
