isEmpty_congr — Mathlib

English

If α is equivalent to β, then IsEmpty α is equivalent to IsEmpty β.

Русский

Если α эквивалентно β, то IsEmpty α эквивалентно IsEmpty β.

LaTeX

$$$$ \\text{IsEmpty }\\alpha \\iff \\text{IsEmpty }\\beta \\quad \\text{given } e: \\alpha \\simeq \\beta. $$$$

Lean4

/-- If `α` is equivalent to `β`, then `IsEmpty α` is equivalent to `IsEmpty β`. -/
theorem isEmpty_congr (e : α ≃ β) : IsEmpty α ↔ IsEmpty β :=
  ⟨fun h => @Function.isEmpty _ _ h e.symm, fun h => @Function.isEmpty _ _ h e⟩

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