self_le_basicOpen_union_iff — Mathlib

English

In an affine open, having the whole open U below the supremum of basic opens generated by a set s is equivalent to the span of s being top.

Русский

В аффинном открытом множество U ниже супрема базисных открытых, образованных из множества s, эквивалентно тому, что порождение s даёт верх.

LaTeX

$$$U \le \bigvee_{f\in s} X.basicOpen f \quad\iff\quad \operatorname{span}(s)=\top$$$

Lean4

theorem self_le_basicOpen_union_iff (s : Set Γ(X, U)) : (U ≤ ⨆ f : s, X.basicOpen f.1) ↔ Ideal.span s = ⊤ :=
  by
  rw [← hU.basicOpen_union_eq_self_iff, @comm _ Eq]
  refine ⟨fun h => le_antisymm h ?_, le_of_eq⟩
  simp only [iSup_le_iff, SetCoe.forall]
  intro x _
  exact X.basicOpen_le x

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