Theorem IsIrreducible.preimage_of_isPreirreducible_fiber

Modification history

2026-02-06 16:14
Mathlib/Topology/Irreducible.lean
refactor(Topology/Irreducible): weaken assumptions of `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` (#33784) …
Added IsIrreducible.preimage_of_isPreirreducible_fiberView on Github →