ball_one_subset_slitPlane — Mathlib

English

The open ball of radius 1 centered at 1 is contained in the slit plane.

Русский

Открытый шар радиуса 1 с центром в 1 содержится в слитной плоскости.

LaTeX

$$\\mathrm{Ball}(1,1) \\subset \\text{slitPlane}$$

Lean4

/-- The slit plane includes the open unit ball of radius `1` around `1`. -/
theorem ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ slitPlane := fun z hz ↦
  .inl <|
    have : -1 < z.re - 1 := neg_lt_of_abs_lt <| (abs_re_le_norm _).trans_lt hz
    by linarith

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