topologyOfClosureOperator_close — Mathlib

English

If c is a closure operator depending on X and the pullback compatibility condition holds, then the close operation of the induced topology equals c X S.

Русский

Если c – замыкающий оператор, зависящий от X, и выполняется условие совместимости вытягивания по стрелкам, то замыкание топологии совпадает с c X S.

LaTeX

$$$(topologyOfClosureOperator\ c\ pb).close S = c\ X\ S$$$

Lean4

theorem topologyOfClosureOperator_close (c : ∀ X : C, ClosureOperator (Sieve X))
    (pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), c Y (S.pullback f) = (c X S).pullback f) (X : C) (S : Sieve X) :
    (topologyOfClosureOperator c pb).close S = c X S := by
  ext Y f
  change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f
  rw [pb, Sieve.mem_iff_pullback_eq_top]

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