image_image'

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.LeftInvOn.image_image'

English

If h is a LeftInvOn f' f s and S₁ ⊆ s then f' '' (f '' S₁) = S₁.

Русский

Если h — левый обратный на s и S₁ ⊆ s, то образ образа S₁ возвращает S₁.

LaTeX

$$$$ (hf.mono \\text{hs}).image\\_image = S_1. $$$$

Lean4

theorem image_image' (hf : LeftInvOn f' f s) (hs : s₁ ⊆ s) : f' '' (f '' s₁) = s₁ :=
  (hf.mono hs).image_image

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

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

Разделы

Аффилиация

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