pretopology_eq_inf — Mathlib

English

Reiterates that pretopology P equals the infimum of jointlySurjectivePretopology and P.pretopology.

Русский

Повторяет, что pretopology P равна пересечению jointlySurjectivePretopology и P.pretopology.

LaTeX

$$$pretopology\\; P = jointlySurjectivePretopology \\cap P.pretopology$$$

Lean4

/-- The pretopology defined by `P`-covers agrees with the
the intersection of the pretopology of surjective families with the pretopology defined by `P`.
-/
theorem pretopology_eq_inf : pretopology P = jointlySurjectivePretopology ⊓ P.pretopology :=
  rfl

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