Theorem CategoryTheory.Functor.mem_inducedTopology_iff_of_isCoverDense

Modification history

2026-06-05 16:26
Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean
refactor(CategoryTheory/Sites): replace `Functor.inducedTopology` (#39951) …
Added CategoryTheory.Functor.mem_inducedTopology_iff_of_isCoverDenseView on Github →