isGLB_sInf — Mathlib

English

For any set T of Pretopology C, sInf T is the greatest lower bound of T in the lattice of coverings.

Русский

Для множества T препотопологий в C искомое sInf T является наибольшей нижней гранью в решётке покрытий.

LaTeX

$$IsGLB T (sInf T)$$

Lean4

theorem isGLB_sInf (T : Set (Pretopology C)) : IsGLB T (sInf T) :=
  IsGLB.of_image (f := fun J ↦ J.coverings) Iff.rfl (_root_.isGLB_sInf _)

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