English
For a,b ∈ ℝ, the frontier of { z : a ≤ Re z ∧ Im z ≤ b } equals the union of the two boundary pieces: Re z = a with Im z ≤ b, or Im z = b with Re z ≥ a.
Русский
Для a,b ∈ ℝ граница множества { z : a ≤ Re z ∧ Im z ≤ b } состоит из двух частей: Re z = a, Im z ≤ b, или Im z = b, Re z ≥ a.
LaTeX
$$$\\operatorname{frontier}\\bigl\\{ z \\in \\mathbb{C} : a \\le \\operatorname{Re} z \\land \\operatorname{Im} z \\le b \\bigr\\} = \\{ z : a \\le \\operatorname{Re} z \\land \\operatorname{Im} z = b \\} \\cup \\{ z : \\operatorname{Re} z = a \\land \\operatorname{Im} z \\le b \\}$$$
Lean4
theorem frontier_setOf_le_re_and_im_le (a b : ℝ) :
frontier {z | a ≤ re z ∧ im z ≤ b} = {z | a ≤ re z ∧ im z = b ∨ re z = a ∧ im z ≤ b} := by
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using frontier_reProdIm (Ici a) (Iic b)
