ofComplex_apply_of_im_nonpos

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.ofComplex_apply_of_im_nonpos

← MathLib Explorer

English

If w.im ≤ 0 then ofComplex w equals a fixed default element (from a choice).

Русский

Если Im(w) ≤ 0, то ofComplex w равняется фиксированному элементу по выбору.

LaTeX

$$ofComplex(w) = Classical.choice inferInstance, if w.im ≤ 0.$$

Lean4

theorem ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) : ofComplex w = Classical.choice inferInstance := by
  simp [ofComplex_apply_eq_ite w, hw]

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

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

Разделы

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

Аффилиация

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