instIsDenseSubsiteRegularTopologyInverse

English

The inverse equivalence induces a dense subsite relationship between regular topologies.

Русский

Обратное эквивалентное отображение порождает плотное подпредставление между регулярными топологиями.

LaTeX

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

Lean4

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

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