boundedSpace_subtype_iff — Mathlib

English

A subtype is bounded if and only if its underlying set is bounded.

Русский

Подтип ограничен тогда и только тогда, когда основанное множество ограничено.

LaTeX

$$$\\text{BoundedSpace}(\\text{Subtype } p) \\iff \\operatorname{IsBounded}\\{x \\mid p(x)\\}$$$

Lean4

theorem boundedSpace_subtype_iff {p : α → Prop} : BoundedSpace (Subtype p) ↔ IsBounded {x | p x} := by
  rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]

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