coe_image — Mathlib

English

The image of a set s under the inclusion ℝ≥0 → ℝ is exactly the set of real numbers that arise as the real part of some element of s.

Русский

Образ множества s при включении ℝ≥0 → ℝ равен множеству вещественных чисел, которые являются действительной частью какого-либо элемента s.

LaTeX

$$$ (\\uparrow) '' s = \\{ x \\in \\mathbb{R} \\; | \\; \\exists h: 0 \\le x, \\; (x,h) \\in s \\}. $$$

Lean4

theorem coe_image {s : Set ℝ≥0} : (↑) '' s = {x : ℝ | ∃ h : 0 ≤ x, @Membership.mem ℝ≥0 _ _ s ⟨x, h⟩} :=
  Subtype.coe_image

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