exists_image_iff — Mathlib

English

For f: α → β, x ⊆ α, and property P on β, there exists an element a in f''x with P(a) iff there exists a in x with P(f(a)).

Русский

Для f: α → β, x ⊆ α и свойство P на β существует элемент a в f''x с P(a) тогда и только тогда, когда существует a в x с P(f(a)).

LaTeX

$$$(\\exists a \\in f''x, P(a)) \\iff (\\exists a \\in x, P(f(a)))$$$

Lean4

theorem exists_image_iff (f : α → β) (x : Set α) (P : β → Prop) : (∃ a : f '' x, P a) ↔ ∃ a : x, P (f a) :=
  ⟨fun ⟨a, h⟩ => ⟨⟨_, a.prop.choose_spec.1⟩, a.prop.choose_spec.2.symm ▸ h⟩, fun ⟨a, h⟩ => ⟨⟨_, _, a.prop, rfl⟩, h⟩⟩

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