English
A variant where closure under op on each open set implies closure under op for sheafified predicate without refinement assumptions.
Русский
Вариант без уточнений: замкнутость под op на каждом открытом множестве в предикате переносится как замкнутость под op после шарирования.
LaTeX
$$$ P.sheafify.pred a \\Rightarrow P.sheafify.pred (fun x => op (a x)). $$$
Lean4
/-- For a unary operation (e.g. `x ↦ -x`) 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 : X → Type*} (P : PrelocalPredicate T) (op : {x : X} → T x → T x)
(hop : ∀ {U : Opens X} {a : (x : U) → T x}, P.pred a → P.pred fun x : U ↦ op (a x)) {U : Opens X}
{a : (x : U) → T x} (ha : P.sheafify.pred a) : P.sheafify.pred (fun x : U ↦ op (a x)) :=
P.sheafify_inductionOn op (fun ha p ↦ ⟨_, 𝟙 _, p.2, hop ha⟩) ha
