ofComplex_apply_eq_ite — Mathlib

English

The value of ofComplex on a complex number w is given by a conditional: it equals the pair (w, proof) when Im(w) > 0, otherwise defined by a chosen default element.

Русский

Значение ofComplex на комплексном числе w задаётся по условию: если Im(w) > 0, то равняется паре (w, доказательство), иначе — некоей выбранной по умолчанию структурой.

LaTeX

$$ofComplex(w) = if hw : 0 < Im(w) then ⟨w, hw⟩ else Classical.choice inferInstance.$$

Lean4

theorem ofComplex_apply_eq_ite (w : ℂ) :
    ofComplex w = if hw : 0 < w.im then ⟨w, hw⟩ else Classical.choice inferInstance :=
  by
  split_ifs with hw
  · exact ofComplex_apply ⟨w, hw⟩
  · change (Function.invFunOn UpperHalfPlane.coe Set.univ w) = _
    simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]
    rintro ⟨a, rfl⟩
    exact (a.prop.not_ge (by simpa using hw)).elim

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