closure_image

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.closure_image

English

Closure of the image equals the image of the closure.

Русский

Замыкание образа равно образу замыкания.

LaTeX

$$$\\mathrm{closure}(f''s) = \\mathrm{map} f(\\mathrm{closure}(s))$$$

Lean4

@[simp]
theorem closure_image (f : M →[L] N) : closure L (f '' s) = map f (closure L s) :=
  (map_closure f s).symm

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

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

Разделы

Аффилиация

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