emptySumLex — Mathlib

English

The lexicographic sum of an empty relation on α with s is isomorphic to s.

Русский

Лексикографическая сумма пустого отношения на α и отношения s изоморфна s.

LaTeX

$$$$ \mathrm{Sum.Lex}\ r\ s \cong_r s \quad [\text{IsEmpty }\ \alpha]. $$$$

Lean4

/-- The lexicographic sum of an empty relation plus `s` is isomorphic to `s`. -/
@[simps!]
def emptySumLex (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : Sum.Lex r s ≃r s :=
  ⟨Equiv.emptySum _ _, by simp⟩

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