smallGrothendieckTopology_eq_toGrothendieck_smallPretopology

English

Equivalence of small Grothendieck topologies under postcomposition properties.

Русский

Эквивалентность малых топологий Гротендика под свойствами посткомпозиции.

LaTeX

$$$S.smallGrothendieckTopologyOfLE hPQ = S.smallGrothendieckTopologyOfLE hPQ$$$

Lean4

theorem smallGrothendieckTopology_eq_toGrothendieck_smallPretopology [P.HasOfPostcompProperty P] :
    S.smallGrothendieckTopology P = (S.smallPretopology P P).toGrothendieck :=
  S.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology le_rfl

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