English
A set belongs to coclosedCompact iff it is contained in some closed compact set via the closure.
Русский
Множество принадлежит coclosedCompact тогда и только тогда, когда оно содержится в замкнутом компактном множестве через замыкание.
LaTeX
$$$s \in \operatorname{coclosedCompact}(X) \iff \operatorname{IsCompact}(\overline{s^c})$$$
Lean4
/-- A set belongs to `coclosedCompact` if and only if the closure of its complement is compact. -/
theorem mem_coclosedCompact_iff : s ∈ coclosedCompact X ↔ IsCompact (closure sᶜ) :=
by
refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩
· rintro ⟨t, ⟨htcl, htco⟩, hst⟩
exact htco.of_isClosed_subset isClosed_closure <| closure_minimal (compl_subset_comm.2 hst) htcl
· exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩
