Theorem preimage_mem_irreducibleComponents

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