preimage_of_isPreirreducible_fiber

English

If V is preirreducible and fibers f⁻¹'{x} are irreducible for all x, then f⁻¹'(V) is preirreducible.

Русский

Если V преднеразложимо и фибры f⁻¹'{x} неразложимы для всех x, то f⁻¹'(V) преднеразложимо.

LaTeX

$$$\mathrm{IsPreirreducible}(V) \rightarrow (f:X\to Y) \rightarrow (\forall x, \mathrm{IsPreirreducible}(f^{-1}({x}))) \rightarrow \mathrm{IsPreirreducible}(f^{-1}(V))$$$

Lean4

theorem preimage_of_isPreirreducible_fiber {V : Set Y} (hV : IsPreirreducible V) (f : X → Y) (hf' : IsOpenMap f)
    (hf'' : ∀ x, IsPreirreducible (f ⁻¹' { x })) : IsPreirreducible (f ⁻¹' V) :=
  by
  refine hV.preimage_of_dense_isPreirreducible_fiber f hf' ?_
  simp [hf'', subset_closure]

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