Irreducible

📁 Source: Mathlib/Topology/Irreducible.lean

Statistics

Metric	Count
Definitions `Irreducible`, `IrreducibleSpace`, `IsIrreducible`, `IsPreirreducible`, `PreirreducibleSpace`, `irreducibleComponent`, `irreducibleComponents`, `irreducibleComponentsEquivOfIsPreirreducibleFiber`	8
Theorems `irreducibleSpace`, `preirreducibleSpace`, `irreducibleSpace_iff`, `isIrreducible_univ`, `toNonempty`, `toPreirreducibleSpace`, `subsingleton_of_isPreirreducible`, `closure`, `image`, `isPreirreducible`, `nonempty`, `of_subtype`, `preimage`, `preimage_of_isPreirreducible_fiber`, `dense`, `closure`, `image`, `interior`, `of_subtype`, `open_subset`, `preimage`, `preimage_of_dense_isPreirreducible_fiber`, `preimage_of_isPreirreducible_fiber`, `subset_irreducible`, `isPreirreducible_univ`, `isPreirreducible`, `irreducibleSpace`, `preirreducibleSpace`, `closure_sUnion_irreducibleComponents_diff_singleton`, `eq_irreducibleComponent`, `exists_mem_irreducibleComponents_subset_of_isIrreducible`, `exists_preirreducible`, `image_mem_irreducibleComponents_of_isPreirreducible_fiber`, `instIrreducibleSpaceCofiniteTopologyOfInfinite`, `instPreirreducibleSpaceOfSubsingleton`, `irreducibleComponent_mem_irreducibleComponents`, `irreducibleComponent_property`, `irreducibleComponents_eq_maximals_closed`, `irreducibleComponents_eq_singleton`, `irreducibleSpace_def`, `isClosed_irreducibleComponent`, `isClosed_of_mem_irreducibleComponents`, `isIrreducible_iff_closure`, `isIrreducible_iff_irreducibleSpace`, `isIrreducible_iff_sInter`, `isIrreducible_iff_sUnion_isClosed`, `isIrreducible_irreducibleComponent`, `isIrreducible_singleton`, `isPreirreducible_empty`, `isPreirreducible_iff_closure`, `isPreirreducible_iff_isClosed_union_isClosed`, `isPreirreducible_iff_preirreducibleSpace`, `isPreirreducible_singleton`, `mem_irreducibleComponent`, `mem_of_subset_sUnion_irreducibleComponents`, `nonempty_preirreducible_inter`, `preimage_mem_irreducibleComponents`, `preimage_mem_irreducibleComponents_of_isPreirreducible_fiber`, `sUnion_irreducibleComponents`, `subset_closure_inter_of_isPreirreducible_of_isOpen`	60
Total	68

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducibleSpace` 📖	mathematical	`Continuous`	`IrreducibleSpace`	—	`range_eq` `Set.image_univ` `IsPreirreducible.image` `PreirreducibleSpace.isPreirreducible_univ` `IrreducibleSpace.toPreirreducibleSpace` `Continuous.continuousOn` `Nonempty.map` `IrreducibleSpace.toNonempty`
`preirreducibleSpace` 📖	mathematical	`Continuous`	`PreirreducibleSpace`	—	`range_eq` `Set.image_univ` `IsPreirreducible.image` `PreirreducibleSpace.isPreirreducible_univ` `Continuous.continuousOn`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducibleSpace_iff` 📖	mathematical	—	`IrreducibleSpace`	—	`Function.Surjective.irreducibleSpace` `continuous` `surjective`

IrreducibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIrreducible_univ` 📖	mathematical	—	`IsIrreducible` `Set.univ`	—	`Set.univ_nonempty` `toNonempty` `PreirreducibleSpace.isPreirreducible_univ` `toPreirreducibleSpace`
`toNonempty` 📖	—	—	—	—	—
`toPreirreducibleSpace` 📖	mathematical	—	`PreirreducibleSpace`	—	—

IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_of_isPreirreducible` 📖	mathematical	`IsDiscrete` `IsPreirreducible`	`Set.Subsingleton`	—	`isDiscrete_iff_forall_exists_isOpen` `Eq.le`

IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`IsIrreducible`	`closure`	—	`isIrreducible_iff_closure`
`image` 📖	mathematical	`IsIrreducible` `ContinuousOn`	`Set.image`	—	`Set.Nonempty.image` `nonempty` `IsPreirreducible.image` `isPreirreducible`
`isPreirreducible` 📖	mathematical	`IsIrreducible`	`IsPreirreducible`	—	—
`nonempty` 📖	mathematical	`IsIrreducible`	`Set.Nonempty`	—	—
`of_subtype` 📖	mathematical	—	`IsIrreducible`	—	`Set.Nonempty.of_subtype` `IrreducibleSpace.toNonempty` `IsPreirreducible.of_subtype` `IrreducibleSpace.toPreirreducibleSpace`
`preimage` 📖	mathematical	`IsIrreducible` `Topology.IsOpenEmbedding` `Set.Nonempty` `Set` `Set.instInter` `Set.range`	`Set.preimage`	—	`preimage_of_isPreirreducible_fiber` `Topology.IsOpenEmbedding.isOpenMap` `Set.Subsingleton.isPreirreducible` `Set.Subsingleton.preimage` `Set.subsingleton_singleton` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding`
`preimage_of_isPreirreducible_fiber` 📖	—	`IsIrreducible` `IsOpenMap` `IsPreirreducible` `Set.preimage` `Set` `Set.instSingletonSet` `Set.Nonempty` `Set.instInter` `Set.range`	—	—	`IsPreirreducible.preimage_of_isPreirreducible_fiber`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense` 📖	mathematical	`IsOpen` `Set.Nonempty`	`Dense`	—	`dense_iff_inter_open` `nonempty_preirreducible_inter`

IsPreirreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`IsPreirreducible`	`closure`	—	`isPreirreducible_iff_closure`
`image` 📖	mathematical	`IsPreirreducible` `ContinuousOn`	`Set.image`	—	`continuousOn_iff'` `Set.inter_comm` `Set.mem_preimage` `Set.mem_image_of_mem` `Set.mem_of_mem_inter_left`
`interior` 📖	mathematical	`IsPreirreducible`	`interior`	—	`open_subset` `isOpen_interior` `interior_subset`
`of_subtype` 📖	mathematical	—	`IsPreirreducible`	—	`Subtype.range_coe` `Set.image_univ` `image` `PreirreducibleSpace.isPreirreducible_univ` `Continuous.continuousOn` `continuous_subtype_val`
`open_subset` 📖	—	`IsPreirreducible` `IsOpen` `Set` `Set.instHasSubset`	—	—	`Set.eq_empty_or_nonempty` `isPreirreducible_empty` `subset_irreducible`
`preimage` 📖	mathematical	`IsPreirreducible` `Topology.IsOpenEmbedding`	`Set.preimage`	—	`preimage_of_isPreirreducible_fiber` `Topology.IsOpenEmbedding.isOpenMap` `Set.Subsingleton.isPreirreducible` `Set.Subsingleton.preimage` `Set.subsingleton_singleton` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding`
`preimage_of_dense_isPreirreducible_fiber` 📖	—	`IsPreirreducible` `IsOpenMap` `Set` `Set.instHasSubset` `closure` `Set.instInter` `setOf` `Set.preimage` `Set.instSingletonSet`	—	—	`mem_closure_iff` `IsOpen.inter`
`preimage_of_isPreirreducible_fiber` 📖	—	`IsPreirreducible` `IsOpenMap` `Set.preimage` `Set` `Set.instSingletonSet`	—	—	`preimage_of_dense_isPreirreducible_fiber` `Set.inter_univ`
`subset_irreducible` 📖	mathematical	`IsPreirreducible` `Set.Nonempty` `IsOpen` `Set` `Set.instHasSubset`	`IsIrreducible`	—	`isIrreducible_iff_sInter` `Finset.coe_insert` `Finset.coe_singleton` `Set.sInter_insert` `Set.sInter_singleton`

PreirreducibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreirreducible_univ` 📖	mathematical	—	`IsPreirreducible` `Set.univ`	—	—

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreirreducible` 📖	mathematical	`Set.Subsingleton`	`IsPreirreducible`	—	—

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducibleSpace` 📖	mathematical	`IsIrreducible`	`IrreducibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`preirreducibleSpace` `IsIrreducible.isPreirreducible` `Set.Nonempty.to_subtype` `IsIrreducible.nonempty`
`preirreducibleSpace` 📖	mathematical	`IsPreirreducible`	`PreirreducibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Set.mem_univ`

(root)

Definitions

Name	Category	Theorems
`Irreducible` 📖	CompData	145 math math: `Prime.irreducible`, `ZMod.irreducible_of_dvd_cyclotomic_of_natDegree`, `Associates.isAtom_iff`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal`, `FixedPoints.minpoly.irreducible`, `Polynomial.cyclotomic.irreducible`, `Polynomial.irreducible_of_mirror`, `Associates.factors_mul`, `Associates.prod_top`, `Associates.finite_factors`, `X_pow_sub_C_irreducible_iff_of_odd`, `Polynomial.irreducible_of_monic`, `X_pow_sub_C_irreducible_of_odd`, `Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three`, `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg`, `FractionalIdeal.count_well_defined`, `MvPolynomial.irreducible_mul_X_add`, `Associates.irreducible_mk`, `not_irreducible_pow`, `Polynomial.IsUnitTrinomial.irreducible_of_coprime`, `irreducible_mul_units`, `PadicInt.irreducible_p`, `Polynomial.exists_monic_irreducible_factor`, `IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg`, `X_pow_sub_C_irreducible_iff_forall_prime_of_odd`, `WeierstrassCurve.Affine.irreducible_polynomial`, `Polynomial.IsUnitTrinomial.irreducible_of_isCoprime`, `Associates.pow_factors`, `Polynomial.irreducible_of_eisenstein_criterion`, `IsSquare.not_irreducible`, `Polynomial.irreducible_mul_leadingCoeff_inv`, `IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal`, `UniqueFactorizationMonoid.irreducible_iff_prime`, `Polynomial.Monic.irreducible_iff_lt_natDegree_lt`, `FractionalIdeal.finprod_heightOneSpectrum_factorization`, `irreducible_subset_of_submonoidClosure_eq_top`, `IsDedekindDomain.HeightOneSpectrum.irreducible`, `Associates.factors_zero`, `Nat.irreducible_iff_prime`, `FractionalIdeal.count_ne_zero`, `Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map`, `MvPolynomial.irreducible_of_forall_totalDegree_le`, `irreducible_or_factor`, `Associates.factors_subsingleton`, `X_pow_sub_C_irreducible_iff_of_prime_pow`, `Associates.factors_mk`, `Polynomial.X_pow_sub_X_sub_one_irreducible`, `MvPolynomial.irreducible_of_disjoint_support`, `IsDiscreteValuationRing.exists_irreducible`, `Polynomial.fact_irreducible_factor`, `IsDiscreteValuationRing.irreducible_iff_uniformizer`, `WfDvdMonoid.not_unit_iff_exists_factors_eq`, `Associates.prod_add`, `Associates.factors_le`, `MvPolynomial.irreducible_sumSMulX`, `Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast`, `PowerSeries.X_irreducible`, `WfDvdMonoid.exists_irreducible_factor`, `isMulIndecomposable_id_univ`, `Associates.factors_mono`, `Associates.factors_eq_some_iff_ne_zero`, `Associates.map_subtype_coe_factors'`, `WittVector.irreducible`, `UniqueFactorizationMonoid.irreducible_of_factor`, `X_pow_sub_C_irreducible_of_prime`, `Polynomial.irreducible_of_degree_eq_one_of_isRelPrime_coeff`, `irreducible_iff_prime_of_exists_prime_factors`, `Polynomial.Monic.irreducible_iff_natDegree`, `Ideal.finite_mulSupport_coe`, `Polynomial.IsUnitTrinomial.irreducible_of_coprime'`, `Polynomial.irreducible_of_degree_le_three_of_not_isRoot`, `Associates.factors_eq_top_iff_zero`, `Cardinal.not_irreducible_of_aleph0_le`, `MulEquiv.irreducible_iff`, `Polynomial.Monic.irreducible_iff_degree_lt`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `not_irreducible_expand`, `PrincipalIdealRing.factors_spec`, `Polynomial.irreducible_factor`, `irreducible_units_mul`, `not_irreducible_zero`, `Associates.irreducible_of_mem_factorSet`, `finite_irreducible`, `not_irreducible_of_not_unit_dvdNotUnit`, `irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree`, `Polynomial.irreducible_iff_degree_lt`, `Polynomial.X_pow_sub_X_sub_one_irreducible_rat`, `DivisorChain.second_of_chain_is_irreducible`, `Polynomial.mem_normalizedFactors_iff`, `not_irreducible_one`, `Associates.irreducible_iff_prime_iff`, `Polynomial.cyclotomic.irreducible_rat`, `Submonoid.FG.finite_irreducible_mem_submonoidClosure`, `X_pow_sub_C_irreducible_of_prime_pow`, `Ideal.finprod_count`, `irreducible_iff`, `Associates.FactorSet.coe_add`, `UniqueFactorizationMonoid.mem_normalizedFactors_iff'`, `Polynomial.isIntegrallyClosed_iff'`, `UniqueFactorizationMonoid.irreducible_of_normalized_factor`, `Polynomial.exists_irreducible_of_natDegree_ne_zero`, `Polynomial.irreducible_X`, `Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff`, `Polynomial.Monic.irreducible_iff_natDegree'`, `Ideal.finprod_heightOneSpectrum_factorization_coe`, `MvPolynomial.irreducible_of_totalDegree_eq_one`, `FractionalIdeal.finite_factors'`, `irreducible_mem_submonoidClosure_subset`, `Polynomial.exists_irreducible_of_natDegree_pos`, `irreducible_mul_iff`, `MvPolynomial.irreducible_sumSMulXSMulY`, `Nat.irreducible_iff_nat_prime`, `Polynomial.not_irreducible_C`, `irreducible_iff_prime`, `Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map`, `WfDvdMonoid.exists_factors`, `associates_irreducible_iff_prime`, `minpoly.irreducible`, `Polynomial.IsEisensteinAt.irreducible`, `Polynomial.irreducible_X_sub_C`, `Submonoid.closure_irreducible`, `Polynomial.irreducible_C_mul_X_add_C`, `Associates.prod_le`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction`, `Polynomial.Monic.irreducible_of_degree_eq_one`, `Ideal.finprod_not_dvd`, `Associated.irreducible_iff`, `Associates.factors_one`, `IsDedekindDomain.HeightOneSpectrum.associates_irreducible`, `Polynomial.irreducible_iff_lt_natDegree_lt`, `Associates.FactorSet.sup_add_inf_eq_add`, `ConjRootClass.irreducible_minpoly`, `Ideal.finite_mulSupport_inv`, `Polynomial.irreducible_of_degree_eq_one`, `irreducible_isUnit_mul`, `Associates.prod_coe`, `irreducible_X_pow_sub_C_of_root_adjoin_eq_top`, `Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three`, `FractionalIdeal.count_coe`, `Associates.FactorSet.prod_eq_zero_iff`, `X_pow_sub_C_irreducible_iff_of_prime`, `Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree`, `Polynomial.exists_irreducible_of_degree_pos`, `isCyclic_tfae`, `irreducible_mul_isUnit`
`IrreducibleSpace` 📖	CompData	19 math math: `AlgebraicGeometry.irreducibleSpace_of_isIntegral`, `AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace`, `Function.Surjective.irreducibleSpace`, `AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat`, `isIrreducible_iff_irreducibleSpace`, `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier`, `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen`, `Subtype.irreducibleSpace`, `Homeomorph.irreducibleSpace_iff`, `AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced`, `AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton`, `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible`, `AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically`, `AlgebraicGeometry.geometricallyIrreducible_iff`, `instIrreducibleSpaceCofiniteTopologyOfInfinite`, `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1`, `PrimeSpectrum.irreducibleSpace`, `AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace`, `irreducibleSpace_def`
`IsIrreducible` 📖	MathDef	29 math math: `PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible`, `isIrreducible_iff_sUnion_isClosed`, `isIrreducible_iff_singleton`, `TopologicalSpace.NoetherianSpace.exists_finset_irreducible`, `TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible`, `PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical`, `isIrreducible_iff_sInter`, `isIrreducible_iff_irreducibleSpace`, `IsGenericPoint.isIrreducible`, `TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed`, `PrimeSpectrum.isIrreducible_zeroLocus_iff`, `TopologicalSpace.IrreducibleCloseds.is_irreducible'`, `PrimeSpectrum.vanishingIdeal_isIrreducible`, `IrreducibleSpace.isIrreducible_univ`, `TopologicalSpace.IrreducibleCloseds.isIrreducible`, `IsPreirreducible.subset_irreducible`, `isIrreducible_singleton`, `TopologicalSpace.IrreducibleCloseds.isIrreducible'`, `TopologicalSpace.IrreducibleCloseds.equivSubtype_apply`, `IsIrreducible.of_subtype`, `TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible`, `TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply`, `TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply`, `PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime`, `isIrreducible_irreducibleComponent`, `irreducibleComponents_eq_maximals_closed`, `isIrreducible_iff_closure`, `irreducibleSpace_def`, `TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply`
`IsPreirreducible` 📖	MathDef	12 math math: `IsPreirreducible.of_subtype`, `isPreirreducible_empty`, `isPreirreducible_iff_preirreducibleSpace`, `isPreirreducible_iff_isClosed_union_isClosed`, `PreirreducibleSpace.isPreirreducible_univ`, `isPreirreducible_iff_closure`, `isPreirreducible_singleton`, `IsIrreducible.isPreirreducible`, `isPreirreducible_iff_forall_mem_subset_closure_singleton`, `irreducibleComponent_property`, `Set.Subsingleton.isPreirreducible`, `isPreirreducible_iff_subsingleton`
`PreirreducibleSpace` 📖	CompData	5 math math: `isPreirreducible_iff_preirreducibleSpace`, `Function.Surjective.preirreducibleSpace`, `instPreirreducibleSpaceOfSubsingleton`, `Subtype.preirreducibleSpace`, `IrreducibleSpace.toPreirreducibleSpace`
`irreducibleComponent` 📖	CompOp	6 math math: `irreducibleComponent_mem_irreducibleComponents`, `mem_irreducibleComponent`, `isIrreducible_irreducibleComponent`, `irreducibleComponent_subset_connectedComponent`, `isClosed_irreducibleComponent`, `irreducibleComponent_property`
`irreducibleComponents` 📖	CompOp	19 math math: `irreducibleComponent_mem_irreducibleComponents`, `genericPoints.component_injective`, `genericPoints.equiv_symm_apply`, `irreducibleComponents_eq_singleton`, `PrimeSpectrum.vanishingIdeal_irreducibleComponents`, `AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe`, `genericPoints.isGenericPoint_ofComponent`, `PrimeSpectrum.zeroLocus_minimalPrimes`, `genericPoints.component_surjective`, `sUnion_irreducibleComponents`, `genericPoints.equiv_apply`, `PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents`, `genericPoints.isGenericPoint`, `AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe`, `TopologicalSpace.NoetherianSpace.finite_irreducibleComponents`, `irreducibleComponents_eq_maximals_closed`, `exists_mem_irreducibleComponents_subset_of_isIrreducible`, `AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian`, `PrimeSpectrum.vanishingIdeal_mem_minimalPrimes`
`irreducibleComponentsEquivOfIsPreirreducibleFiber` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_sUnion_irreducibleComponents_diff_singleton` 📖	mathematical	`Set` `Set.instMembership` `irreducibleComponents`	`closure` `Compl.compl` `Set.instCompl` `Set.sUnion` `Set.instSDiff` `Set.instSingletonSet`	—	`Set.compl_subset_iff_union` `Set.sUnion_singleton` `Set.sUnion_union` `Set.diff_union_of_subset` `Set.singleton_subset_iff` `sUnion_irreducibleComponents` `Set.Subset.antisymm` `IsClosed.closure_subset_iff` `isClosed_of_mem_irreducibleComponents` `Set.inter_eq_right` `subset_closure_inter_of_isPreirreducible_of_isOpen` `Set.sUnion_eq_biUnion` `isOpen_compl_iff` `Set.Finite.isClosed_biUnion` `Set.Finite.diff` `Set.inter_compl_nonempty_iff` `mem_of_subset_sUnion_irreducibleComponents` `Set.diff_subset` `Set.notMem_diff_of_mem` `Set.mem_singleton`
`eq_irreducibleComponent` 📖	—	`IsPreirreducible` `Set` `Set.instHasSubset` `irreducibleComponent`	—	—	`irreducibleComponent_property`
`exists_mem_irreducibleComponents_subset_of_isIrreducible` 📖	mathematical	`IsIrreducible`	`Set` `Set.instMembership` `irreducibleComponents` `Set.instHasSubset`	—	`exists_preirreducible` `IsIrreducible.isPreirreducible` `Set.Nonempty.mono` `Eq.le`
`exists_preirreducible` 📖	mathematical	`IsPreirreducible`	`Set` `Set.instHasSubset`	—	`zorn_subset_nonempty` `Set.mem_sUnion` `IsChain.total` `Set.instReflSubset` `Set.mem_sUnion_of_mem` `Set.subset_sUnion_of_mem` `Maximal.prop` `Maximal.eq_of_subset`
`image_mem_irreducibleComponents_of_isPreirreducible_fiber` 📖	mathematical	`Continuous` `IsOpenMap` `IsPreirreducible` `Set.preimage` `Set` `Set.instSingletonSet` `Set.instMembership` `irreducibleComponents`	`Set.image`	—	`IsIrreducible.image` `Continuous.continuousOn` `IsPreirreducible.preimage_of_isPreirreducible_fiber` `Set.image_subset_iff` `Set.image_preimage_eq` `Set.image_mono`
`instIrreducibleSpaceCofiniteTopologyOfInfinite` 📖	mathematical	—	`IrreducibleSpace` `CofiniteTopology` `CofiniteTopology.instTopologicalSpace`	—	`Set.univ_inter` `Set.compl_union` `compl_compl` `Set.Infinite.nonempty` `Set.Finite.infinite_compl` `Set.Finite.union` `Nontrivial.to_nonempty` `Infinite.instNontrivial`
`instPreirreducibleSpaceOfSubsingleton` 📖	mathematical	—	`PreirreducibleSpace`	—	`Set.Subsingleton.isPreirreducible` `Set.subsingleton_univ_iff`
`irreducibleComponent_mem_irreducibleComponents` 📖	mathematical	—	`Set` `Set.instMembership` `irreducibleComponents` `irreducibleComponent`	—	`isIrreducible_irreducibleComponent` `Eq.le` `eq_irreducibleComponent`
`irreducibleComponent_property` 📖	mathematical	—	`IsPreirreducible` `irreducibleComponent` `Set` `Set.instHasSubset` `Set.instSingletonSet`	—	`exists_preirreducible` `isPreirreducible_singleton`
`irreducibleComponents_eq_maximals_closed` 📖	mathematical	—	`irreducibleComponents` `setOf` `Set` `Maximal` `Set.instLE` `IsClosed` `IsIrreducible`	—	`Set.ext` `isClosed_of_mem_irreducibleComponents` `isClosed_closure` `IsIrreducible.closure` `LE.le.trans` `subset_closure` `le_trans`
`irreducibleComponents_eq_singleton` 📖	mathematical	—	`irreducibleComponents` `Set` `Set.instSingletonSet` `Set.univ`	—	`Set.ext` `IsGreatest.maximal_iff` `IrreducibleSpace.isIrreducible_univ` `Set.subset_univ`
`irreducibleSpace_def` 📖	mathematical	—	`IrreducibleSpace` `IsIrreducible` `Top.top` `Set` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`IrreducibleSpace.isIrreducible_univ`
`isClosed_irreducibleComponent` 📖	mathematical	—	`IsClosed` `irreducibleComponent`	—	`isClosed_of_mem_irreducibleComponents` `irreducibleComponent_mem_irreducibleComponents`
`isClosed_of_mem_irreducibleComponents` 📖	mathematical	`Set` `Set.instMembership` `irreducibleComponents`	`IsClosed`	—	`closure_eq_iff_isClosed` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `subset_closure` `IsIrreducible.closure`
`isIrreducible_iff_closure` 📖	mathematical	—	`IsIrreducible` `closure`	—	`closure_nonempty_iff` `isPreirreducible_iff_closure`
`isIrreducible_iff_irreducibleSpace` 📖	mathematical	—	`IsIrreducible` `IrreducibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Subtype.irreducibleSpace` `IsIrreducible.of_subtype`
`isIrreducible_iff_sInter` 📖	mathematical	—	`IsIrreducible` `Set.Nonempty` `Set` `Set.instInter` `Set.sInter` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.induction_on` `Finset.coe_empty` `Set.sInter_empty` `Set.inter_univ` `IsIrreducible.nonempty` `Finset.coe_insert` `Set.sInter_insert` `Finset.forall_mem_insert` `Set.Finite.isOpen_sInter` `Finset.finite_toSet` `instIsEmptyFalse` `Finset.coe_singleton` `Set.sInter_singleton`
`isIrreducible_iff_sUnion_isClosed` 📖	mathematical	—	`IsIrreducible` `Set` `Finset` `Finset.instMembership` `Set.instHasSubset`	—	`Equiv.forall_congr` `compl_involutive` `Finset.coe_map` `Set.sUnion_image` `Set.iUnion_congr_Prop` `not_imp_not`
`isIrreducible_irreducibleComponent` 📖	mathematical	—	`IsIrreducible` `irreducibleComponent`	—	`mem_irreducibleComponent` `irreducibleComponent_property`
`isIrreducible_singleton` 📖	mathematical	—	`IsIrreducible` `Set` `Set.instSingletonSet`	—	`Set.singleton_nonempty` `isPreirreducible_singleton`
`isPreirreducible_empty` 📖	mathematical	—	`IsPreirreducible` `Set` `Set.instEmptyCollection`	—	—
`isPreirreducible_iff_closure` 📖	mathematical	—	`IsPreirreducible` `closure`	—	`closure_inter_open_nonempty_iff` `IsOpen.inter`
`isPreirreducible_iff_isClosed_union_isClosed` 📖	mathematical	—	`IsPreirreducible` `Set` `Set.instHasSubset`	—	`Function.Surjective.forall` `compl_surjective` `not_imp_not`
`isPreirreducible_iff_preirreducibleSpace` 📖	mathematical	—	`IsPreirreducible` `PreirreducibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Subtype.preirreducibleSpace` `IsPreirreducible.of_subtype`
`isPreirreducible_singleton` 📖	mathematical	—	`IsPreirreducible` `Set` `Set.instSingletonSet`	—	`Set.Subsingleton.isPreirreducible` `Set.subsingleton_singleton`
`mem_irreducibleComponent` 📖	mathematical	—	`Set` `Set.instMembership` `irreducibleComponent`	—	`Set.singleton_subset_iff` `irreducibleComponent_property`
`mem_of_subset_sUnion_irreducibleComponents` 📖	—	`Set` `Set.instMembership` `irreducibleComponents` `Set.instHasSubset` `Set.sUnion`	—	—	`isIrreducible_iff_sUnion_isClosed` `isClosed_of_mem_irreducibleComponents` `Set.Finite.mem_toFinset` `Set.Finite.coe_toFinset` `Set.Subset.antisymm`
`nonempty_preirreducible_inter` 📖	mathematical	`IsOpen` `Set.Nonempty`	`Set` `Set.instInter`	—	`Set.univ_inter` `PreirreducibleSpace.isPreirreducible_univ`
`preimage_mem_irreducibleComponents` 📖	mathematical	`Set` `Set.instMembership` `irreducibleComponents` `Topology.IsOpenEmbedding` `Set.Nonempty` `Set.instInter` `Set.range`	`Set.preimage`	—	`preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` `Topology.IsOpenEmbedding.continuous` `Topology.IsOpenEmbedding.isOpenMap` `Set.Subsingleton.isPreirreducible` `Set.Subsingleton.preimage` `Set.subsingleton_singleton` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding`
`preimage_mem_irreducibleComponents_of_isPreirreducible_fiber` 📖	—	`Set` `Set.instMembership` `irreducibleComponents` `Continuous` `IsOpenMap` `IsPreirreducible` `Set.preimage` `Set.instSingletonSet` `Set.Nonempty` `Set.instInter` `Set.range`	—	—	`IsIrreducible.preimage_of_isPreirreducible_fiber` `Set.image_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `IsIrreducible.closure` `IsIrreducible.image` `Continuous.continuousOn` `Set.image_preimage_eq_inter_range` `subset_closure_inter_of_isPreirreducible_of_isOpen` `IsOpenMap.isOpen_range` `LE.le.trans` `closure_mono` `Set.image_mono`
`sUnion_irreducibleComponents` 📖	mathematical	—	`Set.sUnion` `irreducibleComponents` `Set.univ`	—	`Set.eq_univ_of_forall` `Set.mem_sUnion_of_mem` `mem_irreducibleComponent` `irreducibleComponent_mem_irreducibleComponents`
`subset_closure_inter_of_isPreirreducible_of_isOpen` 📖	mathematical	`IsPreirreducible` `IsOpen` `Set.Nonempty` `Set` `Set.instInter`	`Set.instHasSubset` `closure`	—	`IsClosed.isOpen_compl` `isClosed_closure` `Set.inter_compl_nonempty_iff` `subset_closure`

---

← Back to Index