image_val_subset — Mathlib

English

The first coordinates of elements of γ form a subset of β; i.e., the image of γ under the projection is contained in β.

Русский

Первые координаты элементов γ образуют подмножество β; то есть изображение γ по проекции содержится в β.

LaTeX

$$$\operatorname{image}(\operatorname{Subtype.val}) \gamma \subseteq \beta.$$$

Lean4

theorem image_val_subset : (γ : Set α) ⊆ β :=
  Subtype.coe_image_subset _ _

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