basicOpen_pow — Mathlib

English

The basicOpen is compatible with multiplication: basicOpen(f g) = basicOpen(f) ∩ basicOpen(g).

Русский

basicOpen совместимо с умножением: basicOpen(f g) = basicOpen(f) ∩ basicOpen(g).

LaTeX

$$$X.basicOpen (f g) = X.basicOpen f \cap X.basicOpen g$$$

Lean4

@[simp]
theorem basicOpen_pow {U : Opens X} (f : X.presheaf.obj (op U)) (n : ℕ) (h : 0 < n) :
    X.basicOpen (f ^ n) = X.basicOpen f :=
  by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
  induction k with
  | zero => simp
  | succ n hn => rw [pow_add]; simp_all

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