TopCat.Sheaf.isIso_of_isIso_app_of_isBasis
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace TopCat_Sheaf_isIso_of_isIso_app_of_isBasis
universe u v w u'
open _root_.CategoryTheory Opposite TopologicalSpaceLean source · statement
theorem _root_.TopCat.Sheaf.isIso_of_isIso_app_of_isBasis {C : Type u}
[_root_.CategoryTheory.Category.{v} C] {X : TopCat.{w}}
{ι : Type u'} {B : ι → Opens X} (hB : Opens.IsBasis (Set.range B)) {F G :
TopCat.Sheaf C X} (φ : F ⟶ G)
(h : ∀ i, IsIso (φ.1.app (op (B i)))) : IsIso φ