Theorem IsIrreducible.preimage

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 View on Github →