instIsDenseSubsiteInducedTopologyOfIsCoverDense

Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense

Lean4

instance (priority := 900) [G.IsCoverDense K] : G.IsDenseSubsite (G.inducedTopology K) K where
  functorPushforward_mem_iff := Iff.rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru