exists_congr_right — Mathlib

English

Let e: α ≃ β. Then (∃ a, q(e(a))) ↔ ∃ b, q(b).

Русский

Пусть e: α ≃ β. Тогда (существует a такое, что q(e(a))) эквивалентно ∃b, q(b).

LaTeX

$$$ \forall e:(\alpha \simeq \beta),\ (\exists a:\alpha,\ q(e(a))) \leftrightarrow \ exists b:\beta,\ q(b) $$$

Lean4

protected theorem exists_congr_right : (∃ a, q (e a)) ↔ ∃ b, q b :=
  ⟨fun ⟨_, h⟩ ↦ ⟨_, h⟩, fun ⟨a, h⟩ ↦ ⟨e.symm a, by simpa using h⟩⟩

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