isBounded_image_subtype_val — Mathlib

English

The image of a bounded set under the subtype-embedding val is bounded iff the original set is bounded.

Русский

Образ ограниченного множества под отображением Subtype.val ограничен тогда и только тогда, когда исходное множество ограничено.

LaTeX

$$$\\operatorname{IsBounded}(\\operatorname{Subtype.val} '' s) \\iff \\operatorname{IsBounded}(s)$$$

Lean4

theorem isBounded_image_subtype_val {p : α → Prop} {s : Set { x // p x }} :
    IsBounded (Subtype.val '' s) ↔ IsBounded s :=
  isBounded_induced.symm

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