mem_sInf — Mathlib

English

For a set T of pretopologies, a presieve S on X lies in the infimum sInf T X iff S lies in every t X for t in T.

Русский

Пусть T — множество препотопологий. Предызью S на X принадлежит инфимуму sInf T X тогда, когда S принадлежит каждому t X для всех t из T.

LaTeX

$$$S \\in sInf T X \\iff \\forall t \\in T,\\ S \\in t X$$$

Lean4

theorem mem_sInf (T : Set (Pretopology C)) {X : C} (S : Presieve X) : S ∈ sInf T X ↔ ∀ t ∈ T, S ∈ t X :=
  by
  change S ∈ sInf ((fun J : Pretopology C ↦ J.coverings) '' T) X ↔ _
  simp

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