basicOpen_add_le — Mathlib

English

The basic open of a sum f+g is contained in the union of the basic opens of f and g.

Русский

Базовое открытое суммы f+g содержится в объединении базовых открытых f и g.

LaTeX

$$$X.basicOpen (f + g) \\le X.basicOpen f \\cup X.basicOpen g$$$

Lean4

theorem basicOpen_add_le : X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g :=
  by
  intro x hx
  have hxU : x ∈ U := X.basicOpen_le _ hx
  simp only [SetLike.mem_coe, Scheme.mem_basicOpen _ _ _ hxU, map_add, Opens.coe_sup, Set.mem_union] at hx ⊢
  exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

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