English
For x ∈ A with x_i ≠ 0 for all i, x ∈ negAt s '' (plusPart A) iff ∀ w ∈ s, x.1 w < 0 and ∀ w ∉ s, x.1 w > 0.
Русский
Для x ∈ A с x_i ≠ 0 для всех i, x ∈ negAt s '' (plusPart A) тогда и только тогда, когда ∀ w ∈ s, x_1(w) < 0 и ∀ w ∉ s, x_1(w) > 0.
LaTeX
$$$x \\in A \\\\Rightarrow (\\forall w\\in s, x_1(w)<0) \\land (\\forall w\\notin s, x_1(w)>0) \\iff x \\in negAt(s)''(plusPart(A))$$$
Lean4
theorem mem_negAt_plusPart_of_mem (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
x ∈ negAt s '' (plusPart A) ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) :=
by
refine
⟨fun hx ↦ ⟨fun _ hw ↦ neg_of_mem_negA_plusPart A hx hw, fun _ hw ↦ pos_of_notMem_negAt_plusPart A hx hw⟩,
fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ ‖x.1 w‖, x.2), ⟨(hA x).mp hx₁, fun w ↦ norm_pos_iff.mpr (hx₂ w)⟩, ?_⟩⟩
ext w
· by_cases hw : w ∈ s
· simp [negAt_apply_isReal_and_mem _ hw, abs_of_neg (h₁ w hw)]
· simp [negAt_apply_isReal_and_notMem _ hw, abs_of_pos (h₂ w hw)]
· rfl
