neg_of_mem_negA_plusPart

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.neg_of_mem_negA_plusPart

← MathLib Explorer

English

If x ∈ negAt s '' (plusPart A) and w ∈ s (i.e., w is a real place in s), then x.1 w < 0.

Русский

Если x принадлежит negAt s '' (plusPart A) и w ∈ s, то x_1(w) < 0.

LaTeX

$$$\forall w\in s,\; x_1(w) < 0$$$

Lean4

theorem neg_of_mem_negA_plusPart (hx : x ∈ negAt s '' (plusPart A)) {w : { w // IsReal w }} (hw : w ∈ s) : x.1 w < 0 :=
  by
  obtain ⟨y, hy, rfl⟩ := hx
  rw [negAt_apply_isReal_and_mem _ hw, neg_lt_zero]
  exact hy.2 w

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru