English
A refinement-free version: closure under a binary operation on each open set is preserved under sheafification.
Русский
Версия без уточнений: замкнутость по бинарной операции сохраняется после шарирования.
LaTeX
$$$ P_1.pred a \\land P_2.pred b \\Rightarrow P_3.pred (fun x => op (a x) (b x)) $$$
Lean4
/-- For a binary operation (e.g. `x ↦ y ↦ x + y`) defined at each stalk, if a prelocal predicate is
closed under the operation on each open set, then the sheafified predicate is also closed under the
operation. See `sheafify_inductionOn₂` for the version with refinement. -/
theorem sheafify_inductionOn₂' {X : TopCat} {T₁ T₂ T₃ : X → Type*} (P₁ : PrelocalPredicate T₁)
(P₂ : PrelocalPredicate T₂) (P₃ : PrelocalPredicate T₃) (op : {x : X} → T₁ x → T₂ x → T₃ x)
(hop :
∀ {U V : Opens X} {a : (x : U) → T₁ x} {b : (x : V) → T₂ x},
P₁.pred a → P₂.pred b → P₃.pred fun x : (U ⊓ V : Opens X) ↦ op (a ⟨x, x.2.1⟩) (b ⟨x, x.2.2⟩))
{U : Opens X} {a : (x : U) → T₁ x} {b : (x : U) → T₂ x} (ha : P₁.sheafify.pred a) (hb : P₂.sheafify.pred b) :
P₃.sheafify.pred (fun x : U ↦ op (a x) (b x)) :=
P₁.sheafify_inductionOn₂ P₂ P₃ op (fun ha hb p ↦ ⟨_, Opens.infLELeft _ _, Opens.infLERight _ _, p.2, hop ha hb⟩) ha hb
