English
The union of negAt s '' (plusPart A) over all s equals A provided A is symmetric at real places. Formally, (⋃ s, negAt s '' (plusPart A)) = A.
Русский
Объединение образов negAt s '' (plusPart A) по всем s даёт A при условии симметрии на вещественных местах.
LaTeX
$$$\bigcup_s (negAt(s)''(plusPart(A))) = A$$$
Lean4
/-- Assume that `A` is symmetric at real places then, the union of the images of `plusPart`
by `negAt` and of the set of elements of `A` that are zero at at least one real place
is equal to `A`. -/
theorem iUnion_negAt_plusPart_union : (⋃ s, negAt s '' (plusPart A)) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A :=
by
ext x
rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
refine ⟨?_, fun h ↦ ?_⟩
· rintro (⟨s, ⟨x, ⟨hx, _⟩, rfl⟩⟩ | h)
· simp_rw +singlePass [hA, negAt_apply_norm_isReal, negAt_apply_snd]
rwa [← hA]
· exact h.left
· obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
· exact Or.inr ⟨h, hx⟩
· refine Or.inl ⟨signSet x, (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
· exact lt_of_le_of_ne hw (hx w)
· exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))
