preimage_kernImage

Mathlib.Data.Set.Lattice.Image

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

English

The preimage and kernImage form a Galois connection: preimage f ⊣ kernImage f.

Русский

Прообраз и kernImage образуют связь Галуа: preimage f ⊣ kernImage f.

LaTeX

$$$\\text{preimage f} \\;\\dashv\\; \\text{kernImage f}$$$

Lean4

protected theorem preimage_kernImage : GaloisConnection (preimage f) (kernImage f) := fun _ _ =>
  subset_kernImage_iff.symm

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

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

Разделы

Аффилиация

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