subset_hom — Mathlib

English

For C ∈ G.ComponentCompl L and h: K ⊆ L, the vertex set of C is contained in the vertex set of C.hom h.

Русский

Для C ∈ G.ComponentCompl L и h: K ⊆ L выполняется: множество вершин C содержится в множестве вершин C.hom h.

LaTeX

$$$$ (C:\text{ComponentCompl }L).(\text{setLike.coe})(C) \subseteq (C.\text{hom }h).(\text{setLike.coe}) $$$$

Lean4

theorem subset_hom (C : G.ComponentCompl L) (h : K ⊆ L) : (C : Set V) ⊆ (C.hom h : Set V) :=
  by
  rintro c ⟨cL, rfl⟩
  exact ⟨fun h' => cL (h h'), rfl⟩

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