English
A continuous closed map f carries irreducible closed subsets of X to irreducible closed subsets of Y; this induces a map on irreducible closeds by c ↦ f''c.
Русский
Непрерывное закрытое отображение f переводит неразложимые замкнутые подмножества X в неразложимые замкнутые подмножества Y; следовательно, существует отображение на классы неразложимых замкнутых: c ↦ f''c.
LaTeX
$$$ \forall c \in \operatorname{IrreducibleCloseds}(X),\ f''c \in \operatorname{IrreducibleCloseds}(Y). $$$
Lean4
/-- Map induced on irreducible closed subsets by a closed continuous map `f`.
This is just a wrapper around the image of `f` together with proofs that it
preserves irreducibility (by continuity) and closedness (since `f` is closed).
-/
def map {f : X → Y} (hf1 : Continuous f) (hf2 : IsClosedMap f) (c : IrreducibleCloseds X) : IrreducibleCloseds Y
where
carrier := f '' c
is_irreducible' := c.is_irreducible'.image f hf1.continuousOn
is_closed' := hf2 c c.is_closed'
