exists_subset_image_iff

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.exists_subset_image_iff

English

Disjoint(T, f[S]) ⇔ Disjoint(f^{-1}(T), S).

Русский

Disjoint(T, f[S]) ⇔ Disjoint(f^{-1}(T), S).

LaTeX

$$$\\operatorname{Disjoint}(T, f[S]) \\iff \\operatorname{Disjoint}(f^{-1}(T), S)$$$

Lean4

@[simp]
theorem exists_subset_image_iff {p : Set β → Prop} : (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t) := by
  simp [subset_image_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru