generate_discretePresieve_mem — Mathlib

English

For any α, the sieve generated by the discrete presieve on α lies in the topology on α.

Русский

Для любого α порожденная дискретной презейвой сетка принадлежит топологии α.

LaTeX

$$$ Sieve.generate (discretePresieve α) ∈ typesGrothendieckTopology α $$$

Lean4

theorem generate_discretePresieve_mem (α : Type u) :
    Sieve.generate (discretePresieve α) ∈ typesGrothendieckTopology α := fun x =>
  ⟨PUnit, id, fun _ => x, ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩, rfl⟩

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