∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  IsIrreducible t →
    ∀ (f : Y → X),
      IsOpenMap f → (∀ (x : X), IsPreirreducible (f ⁻¹' {x})) → (t ∩ Set.range f).Nonempty → IsIrreducible (f ⁻¹' t)