coe_mem_upperBounds — Mathlib

English

For a subset s ⊆ ℝ≥0, and any r ∈ ℝ≥0, the relation r ∈ upperBounds (ofNNReal '' s) is equivalent to r ∈ upperBounds s under the natural embedding; i.e. ↑r ∈ upperBounds (ofNNReal '' s) iff r ∈ upperBounds s.

Русский

Для подмножества s ⊆ ℝ≥0 и любого r ∈ ℝ≥0, верно: r ∈ верхних границ (ofNNReal '' s) тогда и только тогда, когда r ∈ верхних границ s, после естественного вложения.

LaTeX

$$$$\\uparrow r \\in \\mathrm{upperBounds}(\\mathrm{ofNNReal}'' s) \\;\\iff\\; r \\in \\mathrm{upperBounds}s$$$$

Lean4

theorem coe_mem_upperBounds {s : Set ℝ≥0} : ↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s := by
  simp +contextual [upperBounds, forall_mem_image, -mem_image, *]

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