instIsDenseSubsiteCoherentTopologyInverse

English

An equivalence gives an IsDenseSubsite between coherent topologies through the inverse direction.

Русский

Эквивалентность задаёт плотное подпредставление между когерентными топологиями через обратное направление.

LaTeX

$$IsDenseSubsite (coherentTopology D) (coherentTopology C) e.inverse$$

Lean4

instance (e : C ≌ D) :
    haveI := precoherent e
    e.inverse.IsDenseSubsite (coherentTopology D) (coherentTopology C)
    where
  functorPushforward_mem_iff := by
    rw [coherentTopology.eq_induced e.inverse]
    simp only [Functor.mem_inducedTopology_sieves_iff, implies_true]

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