Source indexedlemma · leanprover/lean4:v4.32.0

rectangle_disjoint_singleton

PrimeNumberTheoremAnd.Rectangle · PrimeNumberTheoremAnd/Rectangle.lean:144 to 153

Source documentation

Note: try using by simp for h.

Exact Lean statement

lemma rectangle_disjoint_singleton {z w p : ℂ}
    (h : (p.re < z.re ∧ p.re < w.re) ∨ (p.im < z.im ∧ p.im < w.im) ∨
      (z.re < p.re ∧ w.re < p.re) ∨ (z.im < p.im ∧ w.im < p.im)) :
    Disjoint (Rectangle z w) {p}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rectangle_disjoint_singleton {z w p : ℂ}    (h : (p.re < z.re ∧ p.re < w.re) ∨ (p.im < z.im ∧ p.im < w.im) ∨      (z.re < p.re ∧ w.re < p.re) ∨ (z.im < p.im ∧ w.im < p.im)) :    Disjoint (Rectangle z w) {p} := by  refine disjoint_singleton_right.mpr (not_and_or.mpr ?_)  obtain h | h | h | h := h  · exact Or.inl (notMem_uIcc_of_lt h.1 h.2)  · exact Or.inr (notMem_uIcc_of_lt h.1 h.2)  · exact Or.inl (notMem_uIcc_of_gt h.1 h.2)  · exact Or.inr (notMem_uIcc_of_gt h.1 h.2)