image — Mathlib

English

Let s be an irreducible subset of X and f: X → Y be continuous on s. Then the image f[s] is irreducible in Y.

Русский

Пусть s — неразложимое подмножество X, и отображение f: X → Y непрерывно на s. Тогда образ f[s] неразложим в Y.

LaTeX

$$$\mathrm{IsIrreducible}(s) \rightarrow (f:X\to Y) \rightarrow \mathrm{ContinuousOn}(f,s) \rightarrow \mathrm{IsIrreducible}(f''s)$$$

Lean4

@[stacks 0379]
theorem image (H : IsIrreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsIrreducible (f '' s) :=
  ⟨H.nonempty.image _, H.isPreirreducible.image f hf⟩

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