English
If t is preirreducible and f is an open embedding, then the preimage f⁻¹'(t) is preirreducible.
Русский
Если t преднеразложимо и f — открытое вложение, то обратное изображение f⁻¹'(t) преднеразложимо.
LaTeX
$$$\mathrm{IsPreirreducible}(t) \rightarrow (f:\,Y\to X) \rightarrow \mathrm{IsOpenEmbedding}(f) \rightarrow \mathrm{IsPreirreducible}(f^{-1}(t))$$$
Lean4
theorem preimage (ht : IsPreirreducible t) {f : Y → X} (hf : IsOpenEmbedding f) : IsPreirreducible (f ⁻¹' t) :=
by
rintro U V hU hV ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
obtain ⟨_, h₁, ⟨y, h₂, rfl⟩, ⟨y', h₃, h₄⟩⟩ :=
ht _ _ (hf.isOpenMap _ hU) (hf.isOpenMap _ hV) ⟨f x, hx, Set.mem_image_of_mem f hx'⟩
⟨f y, hy, Set.mem_image_of_mem f hy'⟩
cases hf.injective h₄
exact ⟨y, h₁, h₂, h₃⟩
