congr — Mathlib

English

If there are maps f : α → β and g : β → α, then Nonempty α ↔ Nonempty β.

Русский

Если существуют отображения f : α → β и g : β → α, то непусто α эквивалентно непусто β.

LaTeX

$$$\forall {\alpha \beta}, (f : \alpha \to \beta) (g : \beta \to \alpha), \operatorname{Nonempty} \alpha \iff \operatorname{Nonempty} \beta$$$

Lean4

protected theorem congr {α β} (f : α → β) (g : β → α) : Nonempty α ↔ Nonempty β :=
  ⟨Nonempty.map f, Nonempty.map g⟩

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