Theorems · Theorem · general topology

IsIrreducible.preimage_of_isPreirreducible_fiber

∀ {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)

Defined in: Mathlib.Topology.Irreducible
Cited by: 3 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.preimagestatement and proof · cited by 4,946
Set.rangestatement and proof · cited by 4,705
Set.Nonemptystatement and proof · cited by 2,627
IsOpenMapstatement and proof · cited by 253
IsIrreduciblestatement and proof · cited by 59
IsPreirreduciblestatement and proof · cited by 43
IsPreirreducible.preimage_of_isPreirreducible_fiberproof · cited by 3

Cited by3

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.Hom.isIrreducible_preimageproof · cited by 1
preimage_mem_irreducibleComponents_of_isPreirreducible_fiberproof · cited by 1
IsIrreducible.preimageproof · cited by 0