sumDualDistrib — Mathlib

English

The order dual distributes over the binary sum up to an order isomorphism: (OrderDual (Sum α β)) ≃o (OrderDual α) ⊕ (OrderDual β).

Русский

Упорядоченная двойственность распределяется над двоичной суммой до порядка изоморфизма: (OrderDual (Sum α β)) ≃o (OrderDual α) ⊕ (OrderDual β).

LaTeX

$$$ (OrderDual (Sum \alpha \beta)) \cong_o (OrderDual \alpha) \oplus (OrderDual \beta) $$$

Lean4

/-- `orderDual` is distributive over `⊕` up to an order isomorphism. -/
def sumDualDistrib (α β : Type*) [LE α] [LE β] : (α ⊕ β)ᵒᵈ ≃o αᵒᵈ ⊕ βᵒᵈ :=
  { Equiv.refl _ with
    map_rel_iff' := by
      rintro (a | a) (b | b)
      · change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
        simp [toDual_le_toDual, inl_le_inl_iff]
      · exact iff_of_false (@not_inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) not_inr_le_inl
      · exact iff_of_false (@not_inr_le_inl (OrderDual α) (OrderDual β) _ _ _ _) not_inl_le_inr
      · change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
        simp [toDual_le_toDual, inr_le_inr_iff] }

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