mem_basicOpen' — Mathlib

English

A variant of basicOpen with a bundled x shows the same unit condition via germ.

Русский

Вариант basicOpen с упакованной точкой x воспроизводит ту же условие единицы через росток.

LaTeX

$$$\text{mem_basicOpen'}(f,x) := IsUnit( germ_U(x) )$$$

Lean4

/-- A variant of `mem_basicOpen` with bundled `x : U`. -/
@[simp]
theorem mem_basicOpen' {U : Opens X} (f : X.presheaf.obj (op U)) (x : U) :
    ↑x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.germ U x.1 x.2 f) :=
  mem_basicOpen X f x.1 x.2

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