image_fst_graph — Mathlib

English

The image of the graph under the first projection is exactly the support of f.

Русский

Изображение графа под проекцией на первую координату равно опоре функции f.

LaTeX

$$$f.graph.image\\;\\mathrm{fst} = f.support$$$

Lean4

@[simp]
theorem image_fst_graph [DecidableEq α] (f : α →₀ M) : f.graph.image Prod.fst = f.support := by
  classical simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

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