hom_mk — Mathlib

English

The hom map applied to a mk yields the corresponding mk with the adjusted set membership.

Русский

Применение гомоморфизма к конструктору mk равно соответствующему mk с исправленным членством.

LaTeX

$$$$ (G.\text{componentComplMk } vK).hom h = G.componentComplMk (Set.notMem_subset h vK) $$$$

Lean4

theorem hom_mk {v : V} (vnL : v ∉ L) (h : K ⊆ L) :
    (G.componentComplMk vnL).hom h = G.componentComplMk (Set.notMem_subset h vnL) :=
  rfl

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