image_preimage

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.SurjOn.image_preimage

← MathLib Explorer

English

If SurjOn f s t and t₁ ⊆ t, then f''(f⁻¹'(t₁)) = t₁.

Русский

Если SurjOn f s t и t₁ ⊆ t, то f''(f⁻¹'(t₁)) = t₁.

LaTeX

$$$ \mathrm{SurjOn} f s t \land t_1 \subseteq t \rightarrow f''(f^{-1}'(t_1)) = t_1 $$$

Lean4

theorem image_preimage (h : Set.SurjOn f s t) (ht : t₁ ⊆ t) : f '' (f ⁻¹' t₁) = t₁ :=
  image_preimage_eq_iff.2 fun _ hx ↦ mem_range_of_mem_image f s <| h <| ht hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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