English
If P is a property of opens on a scheme X and holds for the bottom element, and if P is preserved under unions with compact open sets, then P holds for all open sets.
Русский
Пусть P — свойство открытых подмножеств схемы X; если оно выполняется для нулевого элемента и сохраняется при объединении с компактными открытыми подмножествами, то оно выполняется для всех открытых подмножеств.
LaTeX
$$$\\text{compact\_open\_induction\_on}(P, S) : P(S) \\text{ under compact unions}$$$
Lean4
@[elab_as_elim]
theorem compact_open_induction_on {P : X.Opens → Prop} (S : X.Opens) (hS : IsCompact S.1) (h₁ : P ⊥)
(h₂ : ∀ (S : X.Opens) (_ : IsCompact S.1) (U : X.affineOpens), P S → P (S ⊔ U)) : P S := by
classical
obtain ⟨s, hs, hs'⟩ := (isCompactOpen_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩
replace hs' : S = iSup fun i : s => (i : X.Opens) := by ext1; simpa using hs'
subst hs'
apply @Set.Finite.induction_on _ _ _ hs
· convert h₁; rw [iSup_eq_bot]; rintro ⟨_, h⟩; exact h.elim
· intro x s _ hs h₄
have : IsCompact (⨆ i : s, (i : X.Opens)).1 := by refine ((isCompactOpen_iff_eq_finset_affine_union _).mpr ?_).1;
exact ⟨s, hs, by simp⟩
convert h₂ _ this x h₄
rw [iSup_subtype, sup_comm]
conv_rhs => rw [iSup_subtype]
exact iSup_insert
