map_sup — Mathlib

English

map distributes over sup: (H1 ⊔ H2).map f = H1.map f ⊔ H2.map f.

Русский

Отображение распределяется по объединению: (H1 ⊔ H2).map f = H1.map f ⊔ H2.map f.

LaTeX

$$$ (H_1 \sqcup H_2).map f = H_1.map f \sqcup H_2.map f $$$

Lean4

theorem map_sup (f : G →g G') (H₁ H₂ : G.Subgraph) : (H₁ ⊔ H₂).map f = H₁.map f ⊔ H₂.map f := by
  ext <;> simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

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