sumLexEmpty — Mathlib

English

The lexicographic sum of a relation r with an empty relation s is isomorphic to r.

Русский

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

LaTeX

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

Lean4

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

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