exists_congr' — Mathlib

English

Let e: α ≃ β. If ∀ b, p(e^{-1}(b)) ↔ q(b), then (∃ a, p(a)) ↔ ∃ b, q(b).

Русский

Пусть e: α ≃ β. Если ∀ b, p(e^{-1}(b)) ↔ q(b), то (∃ a, p(a)) ↔ ∃ b, q(b).

LaTeX

$$$ \forall e:(\alpha \simeq \beta),\ (\forall b:\beta,\ p(e^{-1}(b)) \leftrightarrow q(b)) \rightarrow (\exists a:\alpha,\ p(a)) \leftrightarrow (\exists b:\beta,\ q(b)) $$$

Lean4

protected theorem exists_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

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