image_preimage — Mathlib

English

Let f: A → B. The image operator and the preimage operator form a Galois connection: for all X ⊆ A and Y ⊆ B, image f (X) ⊆ Y iff X ⊆ preimage f (Y).

Русский

Пусть f: A → B. Операторы образа и прообраза образуют связь Галуа: для любых X ⊆ A и Y ⊆ B выполняется image f (X) ⊆ Y тогда и только тогда, когда X ⊆ preimage f (Y).

LaTeX

$$$\\forall X \\subseteq A, Y \\subseteq B:\\, (\\mathrm{image}\, f)(X) \\subseteq Y \\iff X \\subseteq (\\mathrm{preimage}\, f)(Y)$$$

Lean4

protected theorem image_preimage : GaloisConnection (image f) (preimage f) := fun _ _ => image_subset_iff

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