sInf_ofGrothendieck — Mathlib

English

Infimum of Grothendieck topologies, transported to pretopologies, equals the infimum of the image of the topologies under toPretopology.

Русский

Наилучшая нижняя граница топологий Гротендейки после переноса в препотопологии равна инфимуму образа топологий под toPretopology.

LaTeX

$$$\\mathrm{sInf}\,T\\toPretopology = \\mathrm{sInf}(\\mathrm{GrothendieckTopology}.toPretopology''T)$$$

Lean4

theorem sInf_ofGrothendieck (T : Set (GrothendieckTopology C)) :
    (sInf T).toPretopology = sInf (GrothendieckTopology.toPretopology '' T) :=
  by
  ext X S
  simp [mem_sInf, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.mem_sInf]

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