pos_of_notMem_negAt_plusPart

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

← MathLib Explorer

English

If hx ∈ negAt s '' (plusPart A) and w ∉ s, then x.1 w > 0.

Русский

Если hx ∈ negAt s '' (plusPart A) и w ∉ s, тогда x_1(w) > 0.

LaTeX

$$$\forall w \notin s,\; x_1(w) > 0$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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