exists_subset_range_and_iff — Mathlib

English

For any f, p, the statement (∃ S ⊆ range f, p S) is equivalent to ∃ T, p (f'' T).

Русский

Для любой функции f и свойства p подмножество диапазона существует эквивалентно существованию множества T с p(f''T).

LaTeX

$$$ (\\exists S, S \\subseteq \\mathrm{range}(f) \\land p(S)) \\iff (\\exists T, p(\\mathrm{image}(f)(T))). $$$

Lean4

@[simp]
theorem exists_subset_range_and_iff {f : α → β} {p : Set β → Prop} : (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s) := by
  rw [← exists_range_iff, range_image]; rfl

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