invFunOn_image_image_subset

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Function.invFunOn_image_image_subset

← MathLib Explorer

English

For any a in s, invFunOn f s (f a) belongs to s.

Русский

Образ под invFunOn f s от образа f s содержится в s.

LaTeX

$$$$\\big( \\operatorname{invFunOn} f s \\big) '' ( \\operatorname{image} f s ) \\subseteq s.$$$$

Lean4

theorem _root_.Function.invFunOn_image_image_subset [Nonempty α] (f : α → β) (s : Set α) :
    (invFunOn f s) '' (f '' s) ⊆ s := by rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩; exact invFunOn_apply_mem hx

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

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

Разделы

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

Аффилиация

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