Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 19:44 805bb2d2

View on Github →

feat(algebraic_geometry/morphisms): Quasi-compact morphisms of schemes (#15436)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

Created src/algebraic_geometry/morphisms/quasi_compact.lean

added theorem algebraic_geometry.compact_open_induction_on

added theorem algebraic_geometry.is_compact_open_iff_eq_basic_open_union

added theorem algebraic_geometry.is_compact_open_iff_eq_finset_affine_union

added theorem algebraic_geometry.quasi_compact_iff_forall_affine

added theorem algebraic_geometry.quasi_compact_iff_spectral

Modified src/algebraic_geometry/open_immersion.lean

added theorem algebraic_geometry.Scheme.open_cover.Union_range

added theorem algebraic_geometry.Scheme.open_cover.compact_space

Modified src/topology/sets/opens.lean

added theorem topological_space.opens.is_compact_open_iff_eq_finite_Union_of_is_basis

Modified src/topology/subset_properties.lean

added theorem is_compact_open_iff_eq_finite_Union_of_is_topological_basis