disjoint_isReal_isComplex — Mathlib

English

The real infinite places and complex infinite places are disjoint sets.

Русский

Множества реальных и комплексных бесконечных мест попарно не пересекаются.

LaTeX

$$Disjoint { w : InfinitePlace(K) | IsReal w } { w : InfinitePlace(K) | IsComplex w }$$

Lean4

theorem disjoint_isReal_isComplex : Disjoint {(w : InfinitePlace K) | IsReal w} {(w : InfinitePlace K) | IsComplex w} :=
  Set.disjoint_iff.2 <| fun _ hw ↦ not_isReal_iff_isComplex.2 hw.2 hw.1

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