sumEmpty — Mathlib

English

Sum with an empty type is equivalent to the original type: α ⊕ ∅ ≃ α.

Русский

Сумма с пустым типом эквивалентна исходному типу: α ⊕ ∅ ≃ α.

LaTeX

$$$$\alpha \oplus \emptyset \simeq \alpha.$$$$

Lean4

/-- Sum with `IsEmpty` is equivalent to the original type. -/
@[simps symm_apply]
def sumEmpty (α β) [IsEmpty β] : α ⊕ β ≃ α
    where
  toFun := Sum.elim id isEmptyElim
  invFun := inl
  left_inv
    s := by
    rcases s with (_ | x)
    · rfl
    · exact isEmptyElim x

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