codRestrict — Mathlib

English

Given s ⊆ β and f: α →ᵇ β with f(x) ∈ s for all x, the restricted map to s is a bounded continuous map α →ᵇ s.

Русский

Пусть s ⊆ β и f: α →ᵇ β удовлетворяет f(x) ∈ s для всех x. Тогда ограниченное отображение f в s является ограниченно непрерывным отображением α →ᵇ s.

LaTeX

$$$\\operatorname{codRestrict}(s,f,H) \\in \\operatorname{BoundedContinuousFunction} \\\\ α\ \ s$$$

Lean4

/-- Restriction (in the target) of a bounded continuous function taking values in a subset. -/
def codRestrict (s : Set β) (f : α →ᵇ β) (H : ∀ x, f x ∈ s) : α →ᵇ s :=
  ⟨⟨s.codRestrict f H, f.continuous.subtype_mk _⟩, f.bounded⟩

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