frontier_setOf_le_re_and_le_im — Mathlib

English

For a,b ∈ ℝ, the frontier of { z : a ≤ Re z ∧ b ≤ Im z } is the union of the two boundary pieces where either Im z = b or Re z = a.

Русский

Для a,b ∈ ℝ граница множества { z : a ≤ Re z ∧ b ≤ Im z } состоит из двух границ: Im z = b или Re z = a.

LaTeX

$$$\\operatorname{frontier}\\bigl\\{ z \\in \\mathbb{C} : a \\le \\operatorname{Re} z \\land b \\le \\operatorname{Im} z \\bigr\\} \\\\ = \\{ z : a \\le \\operatorname{Re} z \\land \\operatorname{Im} z = b \\} \\cup \\{ z : \\operatorname{Re} z = a \\land b \\le \\operatorname{Im} z \\}$$$

Lean4

theorem frontier_setOf_le_re_and_le_im (a b : ℝ) :
    frontier {z | a ≤ re z ∧ b ≤ im z} = {z | a ≤ re z ∧ im z = b ∨ re z = a ∧ b ≤ im z} := by
  simpa only [closure_Ici, frontier_Ici] using frontier_reProdIm (Ici a) (Ici b)

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