Theorem TopologicalSpace.Opens.IsBasis.of_isInducing

Modification history

2025-05-10 07:53
Mathlib/Topology/Sets/Opens.lean
feat(AlgebraicGeometry): equivalence between ideal sheaves and closed subschemes (#24615)
Added TopologicalSpace.Opens.IsBasis.of_isInducingView on Github →