English
Denote by 𝓂[K] the maximal ideal of the valuation ring 𝒪[K].
Русский
Обозначим 𝓂[K] максимальный идеал кольца ценности 𝒪[K].
LaTeX
$$$\\mathfrak{m}_K \\subseteq \\mathcal{O}_K \\quad \\text{and} \\quad \\mathfrak{m}_K \\text{ is maximal}$$$
Lean4
/-- If for every cell either `A ∩ openCell n j` or `A ∩ closedCell n j` is closed then
`A` is closed. -/
theorem isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell [RelCWComplex C D] [T2Space X] {A : Set X}
(hAC : A ⊆ C) (hDA : IsClosed (A ∩ D))
(h : ∀ n (_ : 0 < n), ∀ (j : cell C n), IsClosed (A ∩ openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A :=
by
rw [closed C A hAC]
refine ⟨?_, hDA⟩
intro n j
induction n using Nat.case_strong_induction_on with
| hz =>
rw [closedCell_zero_eq_singleton]
exact isClosed_inter_singleton
| hi n hn =>
specialize h n.succ n.zero_lt_succ j
rcases h with h1 | h2
· rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1
· exact h2
