Commit 2025-02-28 16:03 c471fbbb

View on Github →

feat(Topology/Sets): define open covers (#21442)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

added theorem AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

modified theorem AlgebraicGeometry.topologically_isLocalAtTarget'

modified theorem AlgebraicGeometry.topologically_isLocalAtTarget

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/Topology/JacobsonSpace.lean

added theorem TopologicalSpace.IsOpenCover.jacobsonSpace_iff

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage

added theorem TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage

added theorem TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage

added theorem TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage

added theorem TopologicalSpace.IsOpenCover.isOpen_iff_inter

modified theorem isOpen_iff_inter_of_iSup_eq_top

Created Mathlib/Topology/Sets/OpenCover.lean

added theorem TopologicalSpace.IsOpenCover.comap

added theorem TopologicalSpace.IsOpenCover.exists_mem

added theorem TopologicalSpace.IsOpenCover.exists_mem_nhds

added theorem TopologicalSpace.IsOpenCover.iSup_eq_top

added theorem TopologicalSpace.IsOpenCover.iSup_set_eq_univ

added theorem TopologicalSpace.IsOpenCover.iUnion_inter

added theorem TopologicalSpace.IsOpenCover.mk

added theorem TopologicalSpace.IsOpenCover.of_sets

added def TopologicalSpace.IsOpenCover

Modified Mathlib/Topology/Sober.lean

added theorem TopologicalSpace.IsOpenCover.quasiSober

added theorem TopologicalSpace.IsOpenCover.quasiSober_iff_forall