topologyOfClosureOperator_self — Mathlib

English

The topology obtained from the closure operator J.closureOperator is equal to J itself.

Русский

Топология, получаемая из оператора замыкания J.closureOperator, равна самой J.

LaTeX

$$$\mathrm{topologyOfClosureOperator}(J_1.closureOperator) = J_1$$$

Lean4

/-- The topology given by the closure operator `J.close` on a Grothendieck topology is the same as `J`.
-/
theorem topologyOfClosureOperator_self :
    (topologyOfClosureOperator J₁.closureOperator fun _ _ => J₁.pullback_close) = J₁ :=
  by
  ext X S
  apply GrothendieckTopology.close_eq_top_iff_mem

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