Commit 2026-02-06 16:14 a63dffee

View on Github →

refactor(Topology/Irreducible): weaken assumptions of preimage_mem_irreducibleComponents_of_isPreirreducible_fiber (#33784) This PR weakens the surjectivity assumption of preimage_mem_irreducibleComponents_of_isPreirreducible_fiber to (t ∩ Set.range f).Nonempty. I also took the liberty of systematizing the file slightly, so that now there are 6 lemmas: preimage of (preirreducible / irreducible / irreducible component) assuming (preirreducible fibers / open embedding).

Estimated changes

Modified Mathlib/Topology/Irreducible.lean

added theorem IsIrreducible.preimage

added theorem IsIrreducible.preimage_of_isPreirreducible_fiber

modified theorem IsPreirreducible.preimage

added theorem preimage_mem_irreducibleComponents