English
Let r ∈ ℝ and s ⊆ sphere(0,r). Then s ⊆ slitPlane iff -r ∉ s.
Русский
Пусть r ∈ ℝ и s ⊆ окружность(центр 0, радиус r). Тогда s ⊆ slitPlane тогда и только тогда, когда -r ∉ s.
LaTeX
$$s \\subseteq \\text{sphere}(0,r) \\Rightarrow ( s \\subseteq \\text{slitPlane} \\iff -r \\notin s)$$
Lean4
/-- A subset of the circle centered at the origin in `ℂ` of radius `r` is a subset of
the `slitPlane` if it does not contain `-r`. -/
theorem subset_slitPlane_iff_of_subset_sphere {r : ℝ} {s : Set ℂ} (hs : s ⊆ sphere 0 r) :
s ⊆ slitPlane ↔ (-r : ℂ) ∉ s :=
by
simp_rw +singlePass [← not_iff_not, Set.subset_def, mem_slitPlane_iff_not_le_zero]
push ¬_
refine ⟨?_, fun hr ↦ ⟨_, hr, by simpa using hs hr⟩⟩
rintro ⟨z, hzs, hz⟩
have : ‖z‖ = r := by simpa using hs hzs
simpa [← this, ← norm_neg z ▸ eq_coe_norm_of_nonneg (neg_nonneg.mpr hz)]
