discreteSieve_mem

Mathlib.CategoryTheory.Sites.Types

URI: https://scilib.ai/kg/mathlib#CategoryTheory.discreteSieve_mem

English

For any α, the discrete sieve on α belongs to the topology typesGrothendieckTopology α.

Русский

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

LaTeX

$$$ discreteSieve\\,α ∈ typesGrothendieckTopology\\,α $$$

Lean4

theorem discreteSieve_mem (α : Type u) : discreteSieve α ∈ typesGrothendieckTopology α := fun x => ⟨x, fun _ => rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru