Theorems · Theorem · category theory

Topology.IsOpenEmbedding.functor_obj_iInf

∀ {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {ι : Type u_1}
  [Nonempty ι] [Finite ι] (g : ι → TopologicalSpace.Opens ↑X), hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i)

Defined in

Mathlib.Topology.Category.TopCat.Opens

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonemptyFinite