L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (map f ⊤)
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (Hom.range f)
rw [Hom.range_eq_map]
no goals
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (map f ⊤)
exact (cg_def.1 h).map f