inclusion — Mathlib

English

Every subset inclusion s ⊆ t defines a continuous map from the subspace s to t, i.e., the inclusion is a continuous map.

Русский

Любое включение подпространств s ⊆ t задаёт непрерывное отображение из s в t; включение непрерывно.

LaTeX

$$$\\mathrm{inclusion}_{s,t}(h) \\in C(s,t)$$$

Lean4

/-- `Set.inclusion` as a bundled continuous map. -/
def inclusion {s t : Set α} (h : s ⊆ t) : C(s, t)
    where
  toFun := Set.inclusion h
  continuous_toFun := continuous_inclusion h

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