mem_sInf — Mathlib

English

For any set s of Grothendieck topologies on C, and sieve S on X, S lies in the infimum sInf s at X iff S lies in every J X for J in s.

Русский

Для множества топологий s на C, и для решётки S на X, S принадлежит sInf s на X тогда и только тогда, когда S принадлежит каждому J X для J ∈ s.

LaTeX

$$S ∈ sInf s X ↔ ∀ t ∈ s, S ∈ t X$$

Lean4

theorem mem_sInf (s : Set (GrothendieckTopology C)) {X : C} (S : Sieve X) : S ∈ sInf s X ↔ ∀ t ∈ s, S ∈ t X :=
  by
  change S ∈ sInf (sieves '' s) X ↔ _
  simp

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