mem_top_basicOpen — Mathlib

English

For the top open, the basic open condition reduces to germ at the global level.

Русский

Для верхнего открытого множества условие basicOpen сводится к ростку на глобальном уровне.

LaTeX

$$$\text{mem_top_basicOpen}(f, x) : x \in basicOpen(f) \iff IsUnit( germ_x(f) )$$$

Lean4

@[simp]
theorem mem_top_basicOpen (f : X.presheaf.obj (op ⊤)) (x : X) : x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.Γgerm x f) :=
  mem_basicOpen X f x .intro

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