exists_mem_target — Mathlib

English

There exists y in e.target with p y if and only if there exists x in e.source with p(e x).

Русский

Существование y в target(e) с p(y) эквивалентно существованию x в source(e) с p(e x).

LaTeX

$$(∃ y ∈ e.target, p y) ↔ (∃ x ∈ e.source, p (e x))$$

Lean4

theorem exists_mem_target {p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x) := by
  rw [← image_source_eq_target, exists_mem_image]

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