disjoint_negAt_plusPart — Mathlib

English

The images of plusPart A under negAt s are pairwise disjoint as s ranges over all places.

Русский

Образы plusPart A под действием negAt s для разных s парно непересекаются.

LaTeX

$$PairwiseDisjoint( { negAt(s) '' (plusPart A) : s } )$$

Lean4

/-- The images of `plusPart` by `negAt` are pairwise disjoint. -/
theorem disjoint_negAt_plusPart : Pairwise (Disjoint on (fun s ↦ negAt s '' (plusPart A))) :=
  by
  intro s t hst
  refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
  obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := Set.symmDiff_nonempty.mpr hst
  · exact lt_irrefl _ <| (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_notMem_negAt_plusPart A hx' hw.2)
  ·
    exact
      lt_irrefl _ <|
        (neg_of_mem_negA_plusPart A hx' hw.1).trans
          (pos_of_notMem_negAt_plusPart A hx hw.2)
            -- We will assume from now that `A` is symmetric at real places

Похожие утверждения