sup — Mathlib

English

Every presieve is contained in its generated sieve: R ≤ generate R.

Русский

Каждый пресейв содержится в порождаемом им свите: R ≤ generate R.

LaTeX

$$R ≤ \\mathrm{generate} R$$

Lean4

/-- The supremum of a collection of sieves: the union of them all. -/
protected def sup (𝒮 : Set (Sieve X)) : Sieve X
    where
  arrows _ := {f | ∃ S ∈ 𝒮, Sieve.arrows S f}
  downward_closed {_ _ f} hf
    _ := by
    obtain ⟨S, hS, hf⟩ := hf
    exact ⟨S, hS, S.downward_closed hf _⟩

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