English
Characterization of codiscrete membership under subtype embedding: a subset U of a subtype S is codiscrete in S iff its image is codiscrete within S.
Русский
Характеризация принадлежности кодискретности подтипу: множество U внутри подтипа S является кодискретным в S тогда и только тогда, когда образ этого множества в S кодискретен внутри S.
LaTeX
$$$U \in codiscrete S \iff (\text{image of } U) \in codiscreteWithin S.$$$
Lean4
theorem mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
U ∈ codiscrete S ↔ (↑) '' U ∈ codiscreteWithin S :=
by
simp only [mem_codiscrete, disjoint_principal_right, compl_compl, Subtype.forall, mem_codiscreteWithin]
congr! with x hx
constructor
· rw [nhdsWithin_subtype, mem_comap]
rintro ⟨t, ht1, ht2⟩
rw [mem_nhdsWithin] at ht1 ⊢
obtain ⟨u, hu1, hu2, hu3⟩ := ht1
refine ⟨u, hu1, hu2, fun v hv ↦ ?_⟩
simpa using fun hv2 ↦ ⟨hv2, ht2 <| hu3 <| by simpa [hv2]⟩
· suffices Tendsto (↑) (𝓝[≠] (⟨x, hx⟩ : S)) (𝓝[≠] x) by convert tendsto_def.mp this _; ext; simp
exact
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ continuous_subtype_val.continuousWithinAt <|
eventually_mem_nhdsWithin.mono (by simp)
